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¶
- 3d: Dependent Data Descriptions for Verified Validation (includes the full documentation of the EverParse Windows binary package)
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