So we have a declarative definition of the valid TLS states that come from the RFC. It's written in Cryptol, and is here: https://github.com/awslabs/s2n/blob/master/tests/saw/spec/rfc-handshake.cry#L134 … now that's done by hand and we have to trust it, it's the "bottom turtle" in the proof, but it's easy to read and review.
It worked ok, but wasn't ideal. We went with SAW/Cryptol because we've been working on a "tied together" verification of all of s2n and there's a lot of benefit in having the cryptography mapped out already in Cryptol.
-
-
I tried F* for it too at HACS, and I think it'd be really good at it, but I didn't get too far.
-
Cryptol should be compatible with lots of other verification tools. We've done manual experiments with F*, full sound equivalence proofs with Coq via an operational semantics, and easycrypt is in the works.
End of conversation
New conversation -
Loading seems to be taking a while.
Twitter may be over capacity or experiencing a momentary hiccup. Try again or visit Twitter Status for more information.