EverParse

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

Our CI maintains up to date Docker images on DockerHub for Linux and Windows

Usage

Example format description files

Complete TLS 1.3 message format of miTLS Bitcoin blocks and transactions

Building

make

Running

./bin/quackyducky -help