What is interesting is that the (core?) of OpenSSL was re-written in Coq according to the author. Then the natural question can that representation be used to generate C code from it and would that make a safer product.
It seems like the author was able to discover the vulnerability while in the process of specifying it in Coq (understanding the handshakes better during specification).
From what I read the Coq specification itself wasn't complete or used to discover the vulnerability.
Would be great if the author shed some light here.
That seems correct. He discovered it while creating the coq specification but coq wasn't itself used to discover the bug. He confirmed that much in this podcast (It's in Japanese though): http://mozaic.fm/post/88061749963/4-security-protocol.
I very much hope that some next big crypto / security library will be designed and tested in some rigorous language like Haskell, its key parts proven correct with something like Coq, and then an efficient and portable implementation code generated automatically.
A C implementation seems inevitable, but an easy-to-link Rust implementation would be very nice to have.
