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.
We produce public releases under the form of a Windows or Linux standalone binary (x86_64) package and a platform-independent source package.
The latest release of EverParse can be found here.
- 3d: Dependent Data Descriptions for Verified Validation (includes the full documentation of the EverParse binary package)
- How to build EverParse from source
In the News¶
- EverParse: Hardening critical attack surfaces with formally proven message parsers;
- Tahina Ramananandro, Aseem Rastogi and Nikhil Swamy; Microsoft Research blog
- Hardening Attack Surfaces with Formally Proven Binary Format Parsers;
- Nikhil Swamy, Tahina Ramananandro, Aseem Rastogi, Irina Spiridonova, Haobin Ni, Dmitry Malloy, Juan Vazquez, Michael Tang, Omar Cardona, Arti Gupta; In Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation, 2022
- DICE*: A Formally Verified Implementation of DICE Measured Boot;
- Zhe Tao, Aseem Rastogi, Naman Gupta, Kapil Vaswani and Aditya V. Thakur; 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; 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
EverParse is Copyright 2018, 2019, 2020, 2021 Microsoft Corporation. All rights reserved. EverParse is free software, licensed by Microsoft Corporation under the Apache License 2.0.
Additionally, the licenses of all dependencies included in the
EverParse binary packages (F*, KaRaMeL, z3, EverCrypt, clang-format) are all
stored in the
licenses/ subdirectory of the EverParse binary
package once extracted.