Comment by dkarapetyan
12 years ago
Honestly, why aren't the formal verification people jumping on this? I keep hearing about automatic code generation from proof systems like Coq and Agda but it's always some toy example like iterative version of fibonacci from the recursive version or something else just as mundane. Wouldn't cryptography be a perfect playground for making new discoveries? At the end of the day all crypto is just number theory and number theory is as formal a system as it gets. Why don't we have formal proofs for correct functionality of OpenSSL? Instead of a thousand eyes looking at pointers and making sure they all point to the right places why don't we formally prove it? I don't mean me but maybe some grad student.
You may be interested in Quark, which is a browser kernel written using Coq http://goto.ucsd.edu/quark/
Yes, why doesn't the same thing exist for SSL? The fact that quark was funded by the NSF means that there is interest in actually doing stuff like this.
Perhaps its time will come soon. That would be really cool.