Portrait of Antoine Delignat-Lavaud

Antoine Delignat-Lavaud

Principal Researcher

About

I’m a Principal Researcher in the Confidential Computing group at MSR Cambridge.

I joined MSR after my PhD at Inria Paris to work on Everest, a project that aims to build and deploy a verified, high-performance implementation of the HTTPS protocol stack in F*, 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 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 is another major spin-off that offers a cross-platform agile API to call various verified implementations of cryptographic primitives coming from HACL* and Vale.

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 for TLS and QUIPS for QUIC.

Nowadays, my focus is on the design of protocols and systems for Confidential Computing services on Azure, such as the Confidential Consortium Framework (CCF), a distributed confidential ledger built on the OpenEnclave 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.