Skip to content

Automated generation of provably secure, zero-copy parsers from format specifications

License

Notifications You must be signed in to change notification settings

dzomo/everparse

This branch is 1242 commits behind project-everest/everparse:master.

Folders and files

NameName
Last commit message
Last commit date

Latest commit

May 14, 2021
8838ecb · May 14, 2021
May 7, 2021
May 12, 2021
Oct 19, 2018
May 14, 2021
Apr 9, 2018
May 6, 2021
May 27, 2020
Feb 14, 2020
May 28, 2020
Jan 8, 2018
May 6, 2021
May 9, 2021
Mar 29, 2021

Repository files navigation

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

About

Automated generation of provably secure, zero-copy parsers from format specifications

Resources

License

Stars

Watchers

Forks

Packages

No packages published

Languages

  • F* 67.2%
  • C 15.9%
  • OCaml 9.7%
  • C++ 4.2%
  • Roff 1.1%
  • Makefile 1.0%
  • Other 0.9%