EverParse

Linux	Windows

EverParse is a framework for generating verified secure parsers from DSL format specification languages. It consists of LowParse, a verified combinator library (in src/lowparse), and QuackyDucky, an untrusted message format specification language compiler.

For more information, you can read:

• The EverParse project website
• our Microsoft Research blog post
• our USENIX Security 2019 paper.

Dependencies

EverParse depends on F* and KreMLin. We recommend to setup your environment using the everest script - it will automate the installation of dependencies (OCaml, opam packages, Z3, Python, F*, etc). Note that setting up an Everest environment from scratch can take time - if you are in a hurry, consider using a containerized build instead.

Container Images

EverParse is part of Project Everest. Everest CI maintains up-to-date Docker Images on Docker Hub for Linux. Those Docker images include a fully built and tested EverParse in the quackyducky subdirectory.

Usage

Example format description files

Complete TLS 1.3 message format of miTLS

Bitcoin blocks and transactions

Building

make

Running

./qd -help