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 (x86_64) package and a platform-independent source package.

The latest release of EverParse can be found here.

Manual

In the News

EverParse: Hardening critical attack surfaces with formally proven message parsers;
Tahina Ramananandro, Aseem Rastogi and Nikhil Swamy; Microsoft Research blog

Papers

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

Licenses

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.

Indices and tables