EverParse

EverParse is a framework for generating verified secure parsers from DSL format specification languages. It consists of several components:

• LowParse, a verified combinator library written in F*, Low* and Pulse
• 3D: A frontend for EverParse to enable specifying data formats in an style resembling type definitions in the C programming language, but with data dependencies. 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.
• EverCBOR, a standalone verified C/Rust implementation of CBOR
• EverCOSign, a standalone verified C/Rust implementation of COSE signing and verification
• EverCDDL, a frontend for EverParse that accepts data formats for CBOR objects in CDDL, and generates verified C or Rust data types, parsers and serializers.

For more information, you can read:

• The EverParse project website and user manual, also available in the doc subdirectory of this repository as *.rst reStructuredText files.
• our CBOR/CDDL/COSE paper (see README-cbor.md for matchings between our paper and the code. The paper has just been accepted to ACM CCS 2025, and has earned the Distinguished Artifact Award!)
• our Microsoft Research blog post
• our PLDI 2022 paper
• our USENIX Security 2019 paper.

Binary packages

Ready-to-use standalone native binary packages for Linux, Windows and MacOS are available as GitHub releases

The contents of the EverParse binary package depends on the platform.

NOTE: Versions 2025.06.05 and earlier only contain 3D and QuackyDucky, and are not available on MacOS.

Docker images

Pre-built Docker Linux images containing everything are available on GitHub Packages. You can run an interactive shell container based on those images using docker run -i -t

Those images are Linux/amd64 only, so on MacOS, you need to install Rosetta and use docker run --platform=linux/amd64

A Dockerfile is available for you to build all of EverParse in a Docker image with docker build -t everparse . and use them in a Docker container with docker run -i -t everparse . On MacOS, you may need to install Rosetta and use docker build --platform=linux/amd64

NOTE: Docker images and Dockerfile are not available for versions 2025.06.05 and earlier.

Usage

3D

See the 3D user manual.

EverCDDL

EverParse presents EverCDDL, our formally verified implementation of CDDL.

NOTE: We finally support table extensibility patterns such as (? 18 => int, * int => any).

The EverCDDL code generator is compiled as an executable, bin/cddl.exe

If you have a CDDL data format description, say mydesc.cddl, you can automatically compile it into C parsers and serializers, with bin/cddl.exe src/cddl/spec/postlude.cddl mydesc.cddl (where src/cddl/spec/postlude.cddl is a subset of the official postlude from RFC 8610). The generated C code links against EverCBOR.

If you want to generate Rust code instead, use the --rust option. Right now, contrary to C, the generated Rust code is standalone and does not need a separate installation of EverCBOR.

More options are available, use --help for more details.

NOTE: EverCDDL currently only supports the deterministic encoding of CBOR. While EverCBOR also offers an implementation for non-deterministic, definite-length CBOR objects, we have not connected it with EverCDDL yet.

QuackyDucky

Run ./bin/qd.exe -help to get instructions on how to run QuackyDucky.

NOTE: Contrary to 3D or EverCDDL, QuackyDucky only produces F* files from data format descriptions. You need to run F* and Karamel by hand to verify the produced files and extract C code:

• The binary package contains F* and Karamel respectively at bin/fstar.exe and bin/krml

• The Docker image contains F* and Karamel respectively at opt/FStar/out/bin/fstar.exe and opt/karamel/krml

TODO: integrate documentation and example by Samuel Chassot

Example format description files

Complete TLS 1.3 message format of miTLS

Bitcoin blocks and transactions

EverCBOR

EverParse presents EverCBOR, our formally verified implementation of CBOR.

We offer two distributions: CBORNondet supports definite-length CBOR objects, and CBORDet supports deterministically encoded CBOR objects (RFC 8979 Section 4.2.1)

NOTE: In both cases, we do not support floating-point values yet. Equivalence of floating-point NaNs for the purpose of map key comparisons has not been fully standardized in IETF CBOR yet; related discussions are ongoing, and we intend to extend our verified implementation with support for floating-point values once such discussions stabilize.

NOTE: Currently, CBORNondet and CBORDet cannot be used together yet.

• C:

  • The generated C source files for the CBOR deterministic encoding are in src/cbor/pulse/det/c, which also contains some tests in the test subdirectory. There, the header file is CBORDet.h. The object file is CBORDet.o, which you can link with your application.

  • A fully documented example is in src/cbor/pulse/det/c/example. There, main.c documents the C API; its Makefile shows how to compile and link against CBORDet.

  • The generated C source files for CBORNondet are in src/cbor/pulse/nondet/c, which also contains some tests in the test subdirectory. There, the header file is CBORNondet.h. The object file is CBORNondet.o, which you can link with your application.

  • A fully documented example is in src/cbor/pulse/nondet/c/example. There, main.c documents the C API; its Makefile shows how to compile and link against CBORNondet.

• Rust:

  • The generated Rust source files for the CBOR deterministic encoding are in src/cbor/pulse/det/rust , where you can use cargo build and cargo test ; the crate is called cborrs.

  • The generated HTML documentation of cborrs is at https://project-everest.github.io/everparse/evercbor-rust/cborrs/

  • TODO: Take a snapshot of the generated Rust source files for CBORNondet

EverCOSign

EverParse presents EverCOSign, our formally verified implementation of COSE signing.

NOTE: Support for encryption is in progress.

• The generated C source files for COSE are in src/cose/c :
  • COSE_Format.c contains the verified parsers and serializers for COSE
  • COSE_EverCrypt.c is a verified implementation of sign1 and verify1 with COSE_Format and HACL* EverCrypt
  • COSE_OpenSSL.c is a handwritten implementation of sign1 and verify1 with OpenSSL, unverified except for parsing and serializing, calling into COSE_Format
• To use the corresponding include files, you need to add src/cbor/pulse/det/c to the include path of your C compiler.
• Interop tests for the C library are in src/cose/interop (OpenSSL) and src/cose/verifiedinterop/test (HACL* EverCrypt)
• The generated Rust source files for COSE are in src/cose/rust, where you can use cargo build and cargo test ; the crate is called evercosign

Building from source

Prerequisites

• On Windows, you need WSL2 (Windows Subsystem for Linux, version 2.x) with Ubuntu 24.04. Then, you will get Linux executables, not Windows. From now on, please follow Ubuntu 24.04 instructions below, which also apply to Windows+WSL2.

• On Ubuntu 24.04 (and Windows+WSL2), EverParse depends on:

  • Rust (for EverCBOR and EverCOSign)

  • A few system packages that can be installed with:

    sudo apt-get install --no-install-recommends ca-certificates curl git pkg-config libffi-dev libgmp-dev libsqlite3-dev libssl-dev time opam

    (opam is not needed by EverCBOR and EverCOSign. libssl-dev is needed only by EverCOSign.)

    For testing, you can install additional packages with:

    sudo apt-get install --no-install-recommends cmake python3-pip python3-venv

• On MacOS, EverParse depends on:

  • Rust (for EverCBOR and EverCOSign)

  • A few Homebrew packages that can be installed with:

    brew install bash gnu-getopt make gnu-time coreutils opam gmp libffi pkgconf sqlite

    (opam is not needed by EverCBOR and EverCOSign.)

    In particular, among these packages is GNU Make. Then, in all build instructions below, replace make with gmake

Build everything

Just run make (gmake on MacOS)

In addition to EverParse, this command will also automatically build all dependencies including opam packages, F*, Karamel and Pulse.

This will take around 1 hour with -j8. However, you do not need to build everything at once: EverParse is composed of several components that you can build individually as you need.

EverCBOR

EverCBOR does not need opam.

• To build the C and Rust CBOR library: run make -f nofstar.Makefile cbor

• To test the C and Rust CBOR library: run make -f nofstar.Makefile cbor-test-unverified

EverCOSign

EverCOSign does not need opam, but needs OpenSSL headers.

• to build the C and Rust COSE library: run make -f nofstar.Makefile cose

• to test the C and Rust COSE library: run make -f nofstar.Makefile cose-extracted-test

EverCDDL

Run make cddl

3D

Run make 3d

QuackyDucky

Run make quackyducky

Build a binary package

To build a standalone native binary package on Linux or MacOS that would work similarly to a GitHub Releases binary package, run one of the following commands:

• make -f package.Makefile everparse to get a directory called everparse containing native binaries for EverParse
• make -f package.Makefile package to get a compressed archive thereof

NOTE: These commands can also be run from Windows+Cygwin with opam installed, to obtain native binary packages for Windows (rather than Linux binaries with WSL2), but only from commits tagged with a GitHub Releases tag. (Such tagged EverParse commits contain sources of F* that can natively build on Windows, which is not the case for the regular F* repository.) In that case, you may need to install additional Cygwin packages by running src/package/windows/install-cygwin-packages.sh beforehand. Then, you can also run make -f package.Makefile nuget to build a NuGet package.

Advanced

Writing F* proofs

If you want to write F* proofs against the EverParse libraries and/or the F* files generated by EverParse, or to contribute to EverParse, you can do it either from the source repository, or from within a Docker image. The following instructions allow you to properly setup Visual Studio Code with the F* VSCode Assistant extension.

In all cases, you can copy the contents of src/package/EverParse.fst.config.json into your configuration file at the root of your workspace directory, to give the extension access to the EverParse proofs. This file refers to an environment variable, EVERPARSE_HOME, which contains the full path to the EverParse clone (/mnt/everparse in the Docker image), as set up by the instructions below.

From the source repository

You can call Visual Studio Code and install the F* VSCode Assistant extension to edit the F* files present in the EverParse repository with full F* editing features.

The configuration files are using a custom F* script, fstar.sh, that sets up the environment properly.

NOTE: On Windows+WSL2, you also need to install the WSL extension, needed to make the Linux paths in the environment variables work.

If you want to do more than just editing files in Visual Studio Code (e.g. run make in subdirectories of EverParse), you need to properly set up environment variables.

You can run a custom Bash shell with ./shell.sh. This script will locally install EverParse dependencies and open a new Bash shell with appropriately populated environment variables for opam, OCaml, F*, etc.

Alternatively, if you are already in a Bash shell session, you can also directly populate its environment with make deps && eval "$(make -s --no-print-directory env)"

From a Docker image

When you start a container from a Docker image for EverParse, its shell is already configured with the proper environment.

Then, you can run Code Server from a container, which allows you to run a web version of Visual Studio Code on your host accessing the F* files in the container:

1. Start a container with docker run -i -t -p 8080:8080

   You can add more options to set up a bind mount to access folders on your host machine.

2. From within the container, run ./start-code-server.sh

3. On your host machine, open a Web browser and go to http://localhost:8080

   This opens a web-based session of Visual Studio Code, accessing the files in the container. The F* VSCode Assistant extension is already installed for you.

Using different F*, Karamel, Pulse clones in opt/

EverParse clones F*, Karamel and Pulse into the opt/ subdirectory. If you want to create an EverParse branch with different clones (e.g. if you need to patch F*, Karamel or Pulse):

1. Change the relevant *_repo variables in opt/Makefile to point to the repositories from which you clone.

2. Run make -C opt snapshot to reflect this change in your clones.

Then, whenever you make a change in your clones:

1. Commit and push your changes.

2. Run make -C opt snapshot to register your clone hashes.

Then, in EverParse, make will automatically rebuild F*, Karamel and Pulse from your clones with your patches.

Using a specific branch of F*, Karamel, Pulse etc.

1. Run make -C opt FStar pulse karamel to clone the default branches of those repositories

2. In the cloned directories, switch to your branch, e.g., git checkout <mybranch>

3. Then run make -C opt snapshot to record the hashes you intend to use

Using an existing opam root, F*, etc.

If you want to use existing dependencies instead of letting EverParse locally install them, you can populate the following environment variables:

• EVERPARSE_USE_OPAMROOT=1 instructs EverParse to use the current opam installation (the value of OPAMROOT if set, otherwise $HOME/.opam) instead of creating a local install

• If you want to use your own F*, first set EVERPARSE_USE_FSTAR_EXE=1, then set FSTAR_EXE to the full path of your fstar.exe executable (by default, fstar.exe via your PATH.)

  NOTE: If you want to use EverCDDL, you cannot use a F* binary package because EverCDDL has a F* plugin that needs to be compiled with the very same OCaml environment as the one used to compile F*. This is why setting EVERPARSE_USE_FSTAR_EXE will automatically set EVERPARSE_USE_OPAMROOT=1.

• If you want to use your own Karamel, first set EVERPARSE_USE_KRML_EXE=1, then set KRML_EXE to the full path of the Karamel executable. This will automatically set EVERPARSE_USE_FSTAR_HOME=1, since the Karamel library must be compiled with the same F* as EverParse.

• If you want to use your own Pulse, first set EVERPARSE_USE_PULSE_HOME=1, then set PULSE_HOME to the full path of the directory where Pulse was compiled (in most cases, the out/ subdirectory of the Pulse clone.) This will automatically set EVERPARSE_USE_FSTAR_HOME=1, since Pulse must be compiled with the same F* as EverParse.

As a shortcut, setting EVERPARSE_USE_MY_DEPS=1 has the same effect as setting all of those environment variables to 1.

NOTES: These settings are all ignored when building a binary package.

NOTE: DO NOT use the clones from the opt/ subdirectory with EVERPARSE_USE_*