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 several 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.

EverCBOR: A verified C and Rust library for CBOR parsing and serialization. Currently, EverCBOR supports the deterministic encoding (RFC 8949 Section 4.2) without floating-point numbers; supporting the full CBOR is work in progress.

EverCDDL: An experimental frontend for EverParse that accepts data formats for CBOR objects in CDDL, and generates C or Rust data types, parsers and serializers. We have used it to generate message processing code for COSE signing.

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.

Those public releases do not contain EverCBOR/EverCDDL. By contrast, we produce pre-built Docker images containing only EverCBOR and EverCDDL

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

Secure Parsing and Serializing with Separation Logic Applied to CBOR, CDDL and COSE;

Tahina Ramananandro, Gabriel Ebner, Guido Martinez, Nikhil Swamy;

32nd ACM SIGSAC Conference on Computer and Communications Security (CCS), 2025 (accepted for publication, to appear)

ASN1*: Provably Correct Non-Malleable Parsing for ASN.1 DER;

Haobin Ni, Antoine Delignat-Lavaud, Cédric Fournet, Tahina Ramananandro, Nikhil Swamy;

In Proceedings of the ACM SIGPLAN international conference on Certified Programs and Proofs (CPP), 2022

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