EverParse: Verified Parsing for Binary Data Formats
Since 2018, as a member of the Research in Software Engineering (RiSE) team at Microsoft Research in Redmond, WA, USA, I have been one of the main authors of EverParse, a formally verified library and front-end for parsing binary data formats.
In recent years, binary data parsing has been one of the most critical software security vulnerabilities, where attackers can take control of systems by crafting ill-formed binary messages not properly rejected by such systems. As one of the main causes of such vulnerabilities, most such parsers have long been written by hand in unsafe languages.
EverParse solves this class of vulnerabilities: users define their data format in a high-level description language, and then push a button to automatically generate efficient parsers proven correct for memory safety, arithmetic safety, functional correctness, unique binary representation, and more. As such, EverParse is a sweet spot in formal verification, providing fully automatic push-button generation of formally verified efficient code with zero user proof effort.
EverParse is formally verified with F*, a 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, and transpiled into efficient low-level languages such as C with KaRaMeL. EverParse is a child of Project Everest (as its name suggests.)
EverParse has successfully been used inside Microsoft products.
EverParse is open-source and its source code is available on GitHub.
Thus far, my work has led to the following publications:
In the News
-
Tahina Ramananandro, Aseem Rastogi, Nikhil Swamy
EverParse: Hardening critical attack surfaces with formally proven message parsers
Microsoft Research Blog, May 3rd, 2021
International peer-reviewed conferences and workshops
-
Haobin Ni,
Antoine Delignat-Lavaud,
Cédric
Fournet,
Tahina Ramananandro,
Nikhil
Swamy
ASN1*: Provably Correct Non-Malleable Parsing for ASN.1 DER
CPP 2023
-
Nikhil
Swamy,
Tahina Ramananandro,
Aseem
Rastogi,
Irina
Spiridonova,
Haobin Ni ,
Dmitry Malloy,
Juan Vazquez,
Michael Tang,
Omar Cardona,
Arti Gupta
Hardening Attack Surfaces with Formally Proven Binary Format Parsers
PLDI 2022
-
Tahina Ramananandro,
Antoine Delignat-Lavaud,
Cédric
Fournet,
Nikhil
Swamy,
Tej Chajed,
Nadim Kobeissi,
Jonathan Protzenko
EverParse: Verified Secure Zero-Copy Parsers for Authenticated Message Formats
USENIX Security 2019