That makes our state machine itself tiny, it's here: https://github.com/awslabs/s2n/blob/master/tls/s2n_handshake_io.c#L253 … all it does is increment a value! Btw one of our coding tenets is never to mix control flow and message parsing in the same function. Big win here!
-
-
The first tool I used to this with what TLA+, because I'd used it before, and we use it to verify state machines elsewhere at AWS, such as our implementations of PAXOS, the state machines at the core of the S3 Load Balancer, AWS HyperPlane, and Elastic Block Store.
-
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.