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.