Involvement in the Everest project
In the Everest project, we aim to specify, implement and formally verify a reference implementation of an HTTPS client and server supporting TLS 1.2 and the upcoming TLS 1.3 protocols. We prove safety, functional correctness and also security (absence of some classes of side channels) for both parts of our implementation, namely the protocol and cryptographic primitives.
To this end, we develop formal verification techniques such as the F* functional programming language with strong dependent types, equipped with a type checker generating verification conditions that are then checked by automatic verification backends such as the Z3 SMT solver. More precisely, most of my work aims to improve the F* user experience (implementation, language front-end, tactics, standard library, memory model) and to provide semantics preservation guarantees for the extraction of F* programs into efficient low-level languages such as C with KreMLin.
Thus far, my work has led to the following publications:
A Monadic Approach to Relational Verification: Applied to Information Security, Program Equivalence, and Optimizations
Verified Low-Level Programming Embedded in F*
Everest: Towards a Verified, Drop-in Replacement of HTTPS