Abstract:
Since 2016, various members of Project Everest have been busy verifying layer after layer of critical software. We started with cryptographic primitives, moved on to high-level stateful APIs, followed by protocols, handshake state machines, and high-level defensive APIs complete with proofs of security in the Dolev-Yao symbolic model. In our most recent work, we tackle the Noise family of protocols, and the MLS secure group messaging protocol.
This talk will recap our journey up the software stack, highlighting the essence of each layer, the challenges we encountered along the way, and how we managed to scale up verification to over 200,000 lines of code. I will focus on the research, but also the engineering, the infrastructure, and all of work that happened behind the scenes and was never mentioned in the papers.
Bio:
I am a Principal Researcher in the RiSE group at Microsoft Research Redmond.
My research focuses on advancing the theory and practice of software verification, i.e. showing with mathematical certainty that a critical piece of code exhibits the intended behavior. This is important for the software industry (e.g. cryptography), but also for society at large (e.g. the law). See our interview in Quanta Magazine for an accessible introduction to verified cryptography, this roundtable on verified cryptography for a research perspective, or this recent CACM Article for a perspective on computational law.
I co-lead the HACL*/EverCrypt verified libraries (among others), and advise Cryspen, a newly-formed startup whose goal is to offer commercial support for the HACL*/EverCrypt ecosystem.
Galois was pleased to host this tech talk via live-stream for the public. A video of the presentation can be found above.