4 ms·

To take it one step further, it might be a good idea to specify the whole thing in Coq, prove correctness and derive the C code from there. Coq is a theorem pro

by zepolud 13y ago

To take it one step further, it might be a good idea to specify the whole thing in Coq, prove correctness and derive the C code from there. Coq is a theorem prover based on the Martin-Löf type theory like the ATS mentioned in the article. Xavier Leroy (the man behind OCaml) managed to write a whole verified C compiler in Coq[1] so while it's slower than writing C directly it should still be feasible for projects of such critical importance. On a related note, mathematicians are also finding it increasingly difficult to trust unverified proofs. Papers by Vladimir Voevodsky, a Fields medalist and one of the most prominent in the field, were also discovered to contain errors more than ten years after publication, having been cited hundreds of times and nobody noticing the errors in the proofs. This was one of the principal motivations for him to initiate the project for homotopy type theory, which also has roots in Martin-Löf type theory and is also being developed formally in Coq. [1]http://compcert.inria.fr/diagram.png http://compcert.inria.fr/diagram.png

anonymousDan 13y ago
It occurs to me that if I was a (black hat) hacker looking for vulnerabilities, I could reimplement critical software in a safe language, leveraging the type checker to search for bugs. Is anyone aware of people doing this already?
- chriswarbo 13y ago
  Your reimplementation would either be very different from the original, and hence not suffer the same bugs, or the compiler wouldn't get further than a couple of function calls before giving you a cryptic error message since it doesn't understand the control flow. Static analysis tools are useful for finding bugs in existing code, but safe programming languages won't magically point out all of the errors in some arbitrary code written in another language. They're safe precisely because they do not allow you to write code in the way that an unsafe language would. As an analogy, if you were looking for use-after-free errors in some C code, it wouldn't do you any good to check a Python version.
  - tokenrove 13y ago
    Actually, your reimplementation can be identical to the original, in a language like ATS, as demonstrated by the article in question. This is one of the things I find very compelling about ATS.
- fulafel 13y ago
  You are on your way to reinventing grammar/model/spec based fuzzing. It works pretty well. Eg. it was used to find the Heartbleed bug (Codenomicon's tools at least, don't know how Google fuzzed it).
jude- 13y ago
I've said it before and I'll say it again. Formalizing the TLS specification and proving that an implementation is consistent with it only shows that the implementation is logically correct. However, it does NOT show that the implementation is secure. Your implementation can be vulnerable to side-channel attacks (particularly timing attacks) while still being logically correct. Proofs of correctness are a (big) step in the right direction, but they're not a silver bullet for building a secure implementation.
- tomp 13y ago
  You can use mathematics to prove other things as well. You could e.g. use a special bool type for all secure data that you can't branch on, so that no secrets could be exposed by examining the runtime path of execution. Or build a model of your CPU's caching and prefetching behaviour and prove that you're code doesn't expose any secrets by that channel.
  - JetSpiegel 13y ago
    How complex must that model be? At least as complex as a real CPU, so we're back on square one.
  - jude- 13y ago
    Right--this will work on some types of side-channel attacks. For example, I could prove that my decryption function runs in a constant amount of time no matter the input. However, you can't proactively defend against side-channel attacks. By definition, a side-channel attack exists because the designer didn't know that the cryptosystem leaks information when (s)he designed and proved the correctness of the implementation. Proving that the cryptosystem doesn't leak information is damn nigh impossible, and often outside the scope of software engineering. My favorite example is acoustic analysis (https://www.cs.tau.ac.il/~tromer/acoustic/ https://www.cs.tau.ac.il/~tromer/acoustic/). Before this was shown to be possible, how were cryptosystem designers supposed to know to defend against it? The best we can do is come up with and formalize a threat model, and then prove that the cryptosystem is secure against the adversaries in the threat model. The problem is that threat models don't help you with adversaries in the future, who have means of getting information from your cryptosystem that you didn't think of.
chotu 13y ago
You can do specification as type in ATS2 too. My biased view is that I find ATS2 to be far more practical than using coq.

by zepolud 13y ago

anonymousDan 13y ago

It occurs to me that if I was a (black hat) hacker looking for vulnerabilities, I could reimplement critical software in a safe language, leveraging the type checker to search for bugs. Is anyone aware of people doing this already?

chriswarbo 13y ago
Your reimplementation would either be very different from the original, and hence not suffer the same bugs, or the compiler wouldn't get further than a couple of function calls before giving you a cryptic error message since it doesn't understand the control flow. Static analysis tools are useful for finding bugs in existing code, but safe programming languages won't magically point out all of the errors in some arbitrary code written in another language. They're safe precisely because they do not allow you to write code in the way that an unsafe language would. As an analogy, if you were looking for use-after-free errors in some C code, it wouldn't do you any good to check a Python version.
- tokenrove 13y ago
  Actually, your reimplementation can be identical to the original, in a language like ATS, as demonstrated by the article in question. This is one of the things I find very compelling about ATS.
fulafel 13y ago
You are on your way to reinventing grammar/model/spec based fuzzing. It works pretty well. Eg. it was used to find the Heartbleed bug (Codenomicon's tools at least, don't know how Google fuzzed it).

jude- 13y ago

I've said it before and I'll say it again. Formalizing the TLS specification and proving that an implementation is consistent with it only shows that the implementation is logically correct. However, it does NOT show that the implementation is secure. Your implementation can be vulnerable to side-channel attacks (particularly timing attacks) while still being logically correct. Proofs of correctness are a (big) step in the right direction, but they're not a silver bullet for building a secure implementation.

tomp 13y ago
You can use mathematics to prove other things as well. You could e.g. use a special bool type for all secure data that you can't branch on, so that no secrets could be exposed by examining the runtime path of execution. Or build a model of your CPU's caching and prefetching behaviour and prove that you're code doesn't expose any secrets by that channel.
- JetSpiegel 13y ago
  How complex must that model be? At least as complex as a real CPU, so we're back on square one.
- jude- 13y ago
  Right--this will work on some types of side-channel attacks. For example, I could prove that my decryption function runs in a constant amount of time no matter the input. However, you can't proactively defend against side-channel attacks. By definition, a side-channel attack exists because the designer didn't know that the cryptosystem leaks information when (s)he designed and proved the correctness of the implementation. Proving that the cryptosystem doesn't leak information is damn nigh impossible, and often outside the scope of software engineering. My favorite example is acoustic analysis (https://www.cs.tau.ac.il/~tromer/acoustic/ https://www.cs.tau.ac.il/~tromer/acoustic/). Before this was shown to be possible, how were cryptosystem designers supposed to know to defend against it? The best we can do is come up with and formalize a threat model, and then prove that the cryptosystem is secure against the adversaries in the threat model. The problem is that threat models don't help you with adversaries in the future, who have means of getting information from your cryptosystem that you didn't think of.

chotu 13y ago

You can do specification as type in ATS2 too. My biased view is that I find ATS2 to be far more practical than using coq.