It's hard to catch these in code reviews because the typical approach is to mix the code that parses messages and the code the proceeds to the next state. For example you might have a parser that handles the first "Hello" message ...
-
-
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.
Show 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 …
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.
Show 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?
Show 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.
Show 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.
Show 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.
Show this thread -
Anyway, that's it unless you want to AMA. I'll just ask
@threadreaderapp to please unroll this thread!Show this thread
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.