Antoine Delignat-Lavaud

À propos

I’m a Principal Researcher in the Confidential Computing (opens in new tab) group at MSR Cambridge.

I joined MSR after my PhD at Inria Paris to work on Everest (opens in new tab), a project that aims to build and deploy a verified, high-performance implementation of the HTTPS protocol stack in F* (opens in new tab), the programming language and verification tool for higher-order, effectful programs that MSR is developing with many academic partners (Inria, CMU, MIT…).

The general verification methodology of Everest is to first write formal high-level specifications, and in some case prove functional correctness properties, then add an idealized specification of the intended security goals of the protocol, and finally write a low-level implementation that is provably safe and correct with respect to the formal specification.

Some of the largest sub-components of Everest are useful in their own right: EverParse (opens in new tab) is a toolchain to automatically produce provably correct, safe and secure zero-copy parsers from declarative binary format specifications. While originally created to process TLS handshake messages, it has been generalized to support a large class of applications, and can be used by developers without verification background or knowledge of F*. EverCrypt (opens in new tab) is another major spin-off that offers a cross-platform agile API to call various verified implementations of cryptographic primitives coming from HACL* (opens in new tab) and Vale (opens in new tab).

Besides its toolchain and artefacts, an important part of the impact of Everest is to influence the design of the new generation of security protocols. Our formal specifications and security models have served as an input for the standardization of the TLS 1.3 and QUIC protocols at the IETF, thanks to the joint academic and industry events such as TRON (opens in new tab) for TLS and QUIPS (opens in new tab) for QUIC.

Nowadays, my focus is on the design of protocols and systems for Confidential Computing (opens in new tab) services on Azure, such as the Confidential Consortium Framework (opens in new tab) (CCF), a distributed confidential ledger built on the OpenEnclave (opens in new tab) SDK. An important goal of confidential computing is to replace trust assumptions in the Azure platform with technical guarantees from remote attestation. This requires a new range of protocols and services to control the trusted computing base of core Azure services, such as Key Vault for key management and Storage.