4 ms·

I think this similar to what ADA is doing in crypto space.

by dk8996 6y ago

exdsq 6y ago
I don’t understand what “hacker-proof code means”, but yes IOHK (who develop Cardano) do use formal methods such as Isabelle and Coq alongside some process specification languages.
- MaxBarraclough 6y ago
  > I don’t understand what “hacker-proof code means” What's unclear about it?
  - serf 6y ago
    it's not that it's unclear per se, it's just an untenable position to take. lazy example : a hardware-level side-channel attack is not rendered impossible simply because the software was made with formal verification methods.
  - aspenmayer 6y ago
    Code can’t confer immunity to attacks outside the scope of verification methods as implemented. As another poster mentioned above, side channel attacks or hardware vulnerabilities are outside the scope and capabilities of formal verification methods’ ability to mitigate or mediate directly. Which is not to say be verification could be improved to account for this. But if you knew there were no bugs already due to formal verification I guess at least these unknown bugs are likewise much more limited in scope and offset by entire classes of bugs determined to not be present.
  - exdsq 6y ago
    You can't verify the OS, you can't verify the network connection between your apps, you can't account for poor business requirements that result in formally verified hackable code, etc...
    - MaxBarraclough 6y ago
      > You can't verify the OS You can. Look at seL4. This is an area of ongoing research. > you can't verify the network connection between your apps In what sense? You can verify the crypto, and the networking stack. > you can't account for poor business requirements that result in formally verified hackable code Not sure what you're saying here. Are you referring to the possibility that the formal specification might not be adequate to guarantee security, even discounting side-channel attacks?

4 ms·

I think this similar to what ADA is doing in crypto space.

by dk8996 6y ago

I think this similar to what ADA is doing in crypto space.

exdsq 6y ago
I don’t understand what “hacker-proof code means”, but yes IOHK (who develop Cardano) do use formal methods such as Isabelle and Coq alongside some process specification languages.
- MaxBarraclough 6y ago
  > I don’t understand what “hacker-proof code means” What's unclear about it?
  - serf 6y ago
    it's not that it's unclear per se, it's just an untenable position to take. lazy example : a hardware-level side-channel attack is not rendered impossible simply because the software was made with formal verification methods.
  - aspenmayer 6y ago
    Code can’t confer immunity to attacks outside the scope of verification methods as implemented. As another poster mentioned above, side channel attacks or hardware vulnerabilities are outside the scope and capabilities of formal verification methods’ ability to mitigate or mediate directly. Which is not to say be verification could be improved to account for this. But if you knew there were no bugs already due to formal verification I guess at least these unknown bugs are likewise much more limited in scope and offset by entire classes of bugs determined to not be present.
  - exdsq 6y ago
    You can't verify the OS, you can't verify the network connection between your apps, you can't account for poor business requirements that result in formally verified hackable code, etc...
    - MaxBarraclough 6y ago
      > You can't verify the OS You can. Look at seL4. This is an area of ongoing research. > you can't verify the network connection between your apps In what sense? You can verify the crypto, and the networking stack. > you can't account for poor business requirements that result in formally verified hackable code Not sure what you're saying here. Are you referring to the possibility that the formal specification might not be adequate to guarantee security, even discounting side-channel attacks?