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.

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

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