Tahina Ramananandro > Research >

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 overview

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

International peer-reviewed conferences and workshops