We then use SAW to map our s2n_handshake C code to something that can be symbolically executed for all possible inputs. Here's the SAW code that does the mapping: https://github.com/awslabs/s2n/blob/master/tests/saw/s2n_handshake_io.saw …
-
Show this thread
-
So together, these actually check that our handshake code really does all TLS valid state transitions correctly, and only those. We caught bugs when we first added it too! Not a security issue, but it turns out we didn't support an obscure combination of OSCP and resumption.
1 reply 1 retweet 13 likesShow this thread -
Now my favorite part ... how do we know that the verification itself actually works? We run it on every build, but what does that say?
1 reply 0 retweets 7 likesShow this thread -
We *also* "verify the verifier" by forcing some negative test cases. We actually patch the code with known errors: https://github.com/awslabs/s2n/tree/master/tests/saw/failure_tests … and check that the formal verification fails! This is super important for checking formal verf btw, and often overlooked.
2 replies 8 retweets 55 likesShow this thread -
We also do fuzz tests (https://github.com/awslabs/s2n/tree/master/tests/fuzz …) and we have integration tests with other implementations, to check for inter-op.
2 replies 0 retweets 16 likesShow this thread -
Our goal with tooling is to ensure that we have failsafes beyond code-review. For these state machine type bugs, it actually takes quite a lot! There's a lot more code verifying it than implementing it. It's not surprising that these issues crop up in real world software.
1 reply 3 retweets 30 likesShow this thread -
Anyway, that's it unless you want to AMA. I'll just ask
@threadreaderapp to please unroll this thread!5 replies 0 retweets 28 likesShow this thread -
Replying to @BRIAN_____ @threadreaderapp
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.
1 reply 0 retweets 2 likes -
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.
1 reply 0 retweets 0 likes
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.
0 replies 0 retweets 2 likesThanks. Twitter will use this to make your timeline better. UndoUndo
-
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.