Verified efficient parsing for binary data formats

EverParse is a framework for generating verified secure parsers and formatters from domain-specific format specification languages.

The framework contains three components:

LowParse: At the core of EverParse is LowParse, a verified library of parsing and formatting combinators programmed and verified in F*.

3D: A frontend for EverParse to enable specifying data formats in an style resembling type definitions in the C programming language. We have used it to generate message validation code for use within several low-level C programs.

QuackyDucky: A frontend for EverParse that accepts data formats in a style common to many RFCs. We have used it to generate message processing code for several networking protocols, including TLS and QUIC.

EverParse is open-source and available on GitHub. EverParse is part of Project Everest.

Releases

We produce public releases under the form of a Windows or Linux standalone binary (amd64) package and a platform-independent source package.

The latest release of EverParse can be found here.

Manual

Papers

DICE*: A Formally Verified Implementation of DICE Measured Boot;
Zhe Tao, Aseem Rastogi, Naman Gupta, Kapil Vaswani and Aditya V. Thakur; To appear in Proceedings of the 30th USENIX Security Symposium, 2021
A Security Model and Fully Verified Implementation for the IETF QUIC Record Layer;
Antoine Delignat-Lavaud, Cedric Fournet, Bryan Parno, Jonathan Protzenko, Tahina Ramananandro, Jay Bosamiya, Joseph Lallemand, Itsaka Rakotonirina, and Yi Zhou; To appear in Proceedings of the 42nd IEEE Symposium on Security and Privacy, 2021
EverParse: Verified Secure Zero-Copy Parsers for Authenticated Message Formats;
Tahina Ramananandro, Antoine Delignat-Lavaud, Cedric Fournet, Nikhil Swamy, Tej Chajed, Nadim Kobeissi, and Jonathan Protzenko; In Proceedings of the 28th USENIX Security Symposium, 2019

Indices and tables