Skip to content

Latest commit

 

History

History
36 lines (23 loc) · 2.27 KB

README.md

File metadata and controls

36 lines (23 loc) · 2.27 KB

EverParse

Linux Windows
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:

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