The title of my thesis is: “Formal Verification for High Assurance Security Software in F*”.
The thesis manuscript. The slides of the defense.

The defense focused on how to build formally verified C artifacts such as a cryptographic library (HACL*), scale the approach to protocol libraries (TLS, Signal*) and how to use this experience to design and prove secure new protocols such as Messaging Layer Security (MLS).

The PhD committee:

  • Véronique Cortier, reviewer and president
  • Gilles Barthe, reviewer
  • Cas Cremers, examiner
  • Eric Rescorla, examiner
  • Peter Schwabe, examiner
  • Karthik Bhargavan, PhD supervisor