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