4 ms·
Preferably something generated from a formal proof tool. It wouldn't be perfect (nothing is), but the mistakes would be less stupid. Which is a big jump! The
by lallysingh 13y ago
Preferably something generated from a formal proof tool. It wouldn't be perfect (nothing is), but the mistakes would be less stupid. Which is a big jump!
There's a bit of research in this, but I don't know of anything that's ready to use.
- dllthomas 13y agoWell, there's Coq, which (per my understanding) may or may not make the cut depending on how you define "ready to use".
- lallysingh 13y agoI know Coq as a tool to help generate proofs. Does it generate code? Either way, it's not a verified implementation of TLS. For that, we'd need: (1) A set of properties to verify for an implementation (2) An implementation to verify Looking at http://coq.inria.fr/related-tools http://coq.inria.fr/related-tools, there may be some related tools that could do the job. Still, there's a research project there.
- dllthomas 13y agoPeople absolutely use Coq to generate code. I don't know what else is involved. A few substantiating links from my search results for "coq generating code": http://coq.inria.fr/V8.1/refman/Reference-Manual021.html http://coq.inria.fr/V8.1/refman/Reference-Manual021.html http://research.microsoft.com/en-us/um/people/akenn/coq/LOLA2012.pdf http://research.microsoft.com/en-us/um/people/akenn/coq/LOLA... http://research.microsoft.com/en-us/um/people/nick/coqasm.pdf http://research.microsoft.com/en-us/um/people/nick/coqasm.pd...
- lallysingh 13y agoOh great! Thanks. Upvoted.
- e12e 13y agoMaybe ADA SPARK?: http://senier.net/libsparkcrypto/ http://senier.net/libsparkcrypto/