Skip to content
No description, website, or topics provided.
HTML CSS
Branch: master
Clone or download
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
Type Name Latest commit message Commit time
Failed to load latest commit information.
_layouts
assets/css
README.md

README.md

TIE: TLS Invariants Exploration

Ben Lowman

Problem

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.

Goal

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.

Resources

  • 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...
You can’t perform that action at this time.