Involvement in the Everest project
Since 2016, I have been collaborating on the Everest project, as a member of the Research in Software Engineering (RiSE) team at Microsoft Research in Redmond, WA, USA.
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 KaRaMeL.
Thus far, my work has led to the following publications:
EverParse
One child of Project Everest has been EverParse: formally verified parsers for binary data formats. You can read my separate page listing my EverParse-related publications.
International peer-reviewed conferences and workshops
-
Aymeric Fromherz,
Aseem
Rastogi,
Nikhil
Swamy,
Sydney Gibson,
Guido
Martínez,
Denis Merigoux,
Tahina Ramananandro
Steel: Proof-oriented Programming in a Dependently Typed Concurrent Separation Logic
ICFP 2021
-
Antoine Delignat-Lavaud,
Cédric
Fournet,
Bryan Parno,
Jonathan Protzenko,
Tahina Ramananandro,
Jay Bosamiya,
Joseph Lallemand,
Itsaka Rakotonirina,
Yi Zhou
A Security Model and Fully Verified Implementation for the IETF QUIC Record Layer
IEEE S&P 2021 ("Oakland")
-
Jonathan Protzenko,
Bryan Parno,
Aymeric Fromherz,
Chris
Hawblitzel,
Marina Polubelova,
Karthikeyan Bhargavan,
Benjamin Beurdouche,
Joonwon Choi,
Antoine Delignat-Lavaud,
Cédric
Fournet,
Natalia Kulatova,
Tahina Ramananandro,
Aseem
Rastogi,
Nikhil
Swamy,
Christoph
Wintersteiger,
Santiago
Zanella-Béguelin
EverCrypt: A Fast, Verified, Cross-Platform Cryptographic Provider
IEEE S&P 2020 ("Oakland")
-
Guido
Martínez,
Danel Ahman,
Victor Dumitrescu,
Nick Giannarakis,
Chris
Hawblitzel,
Catalin
Hritcu,
Monal Narasimhamurthy,
Zoe Paraskevopoulou,
Clément Pit-Claudel,
Jonathan Protzenko,
Tahina Ramananandro,
Aseem
Rastogi,
Nikhil
Swamy
Meta-F*: Proof Automation with SMT, Tactics and Metaprograms
ESOP 2019
-
Niklas Grimm,
Kenji Maillard,
Cédric
Fournet,
Catalin
Hritcu,
Matteo
Maffei,
Jonathan Protzenko,
Tahina Ramananandro,
Aseem
Rastogi,
Nikhil
Swamy,
Santiago
Zanella-Béguelin
A Monadic Approach to Relational Verification: Applied to Information Security, Program Equivalence, and Optimizations
CPP 2018
-
Jonathan Protzenko,
Jean-Karim Zinzindohoué,
Aseem
Rastogi,
Tahina Ramananandro,
Peng Wang,
Santiago Zanella-Béguelin,
Antoine Delignat-Lavaud,
Catalin Hritcu,
Karthikeyan Bhargavan,
Cédric Fournet,
Nikhil Swamy
Verified Low-Level Programming Embedded in F*
ICFP 2017
-
Karthikeyan Bhargavan,
Barry Bond,
Antoine Delignat-Lavaud,
Cédric Fournet,
Chris
Hawblitzel,
Catalin Hritcu,
Samin Ishtiaq,
Markulf Kohlweiss,
Rustan Leino,
Jay Lorch,
Kenji Maillard,
Jianyang Pang,
Bryan Parno,
Jonathan Protzenko,
Tahina Ramananandro,
Ashay Rane,
Aseem
Rastogi,
Nikhil Swamy,
Laure Thompson,
Peng Wang,
Santiago Zanella-Béguelin,
Jean-Karim Zinzindohoué
Everest: Towards a Verified, Drop-in Replacement of HTTPS
SNAPL 2017