O.k. so that's the basic approach, but how do we then test it? how do we make sure that all of our valid states are correct? With some help from @galois , we formally verify it! Here's how ...
-
Show this thread
-
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.
2 replies 1 retweet 34 likesShow this thread -
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 …
2 replies 0 retweets 10 likesShow 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
That's not automated, but thankfully it doesn't change much. There's only so many TLS extensions!
-
-
Replying to @chadloder
Thank to YOU!
If you want you can support me: https://threadreaderapp.com/account/premium 0 replies 0 retweets 0 likes
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.