Implementing TLS is hard. Given the wide range of cipher suites, target platforms, and legacy code, it is unlikely that any TLS implementations are free of bugs (see Heartbleed, Apple's goto fail, CCS injection, etc.). Rigorous testing is required in cases where formal verification is not feasible. For most implementations, traditional software engineering techniques are the primary means by which confidence is gained in the correctness of the implementation.
My goal is to explore the use of program invariants in testing TLS implementations. Inferred program invariants are a compressed expression of program state, independent of control flow or output. Dynamically inferred invariants (over test cases) could be compared to ground truth invariants as a more robust method to verify program correctness. It is also likely that different TLS implementations exhibit similar invariants. I am interested in exploring the possibility of employing Frankencerts-type differential testing over dynamically inferred program invariants in addition to expected output. This will require abstracting program invariants in a meaningful way so that such "similar" invariants can be compared directly.
- Frankencerts paper, and a follow-up paper that uses line coverage to guide certificate generation.
- Daikon, a tool for dynamically detecting possible program invariants. There are dozens of papers listed that leverage Daikon.
- SourcererCC, a fast, token based code clone detector. This might aid in finding "similar" code across TLS implementations.
- Microsoft's miTLS implementation. This implementation is annotated with invariants (required for the formal verification).
- To be continued...