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 and user manual, also available in the
doc
subdirectory of this repository as*.rst
reStructuredText files. - our CBOR/CDDL/COSE paper draft (see
README-cbor.md
for matchings between our paper and the code. The paper has just been accepted to ACM CCS 2025.) - our Microsoft Research blog post
- our PLDI 2022 paper
- our USENIX Security 2019 paper.
This section is focused on build and usage instructions. For more details on the proofs, see README-cbor.md
A Dockerfile
is available for you to build CBOR, CDDL and COSE in a Docker image
with docker build -t evercddl .
and use them in a Docker container
with docker run -i -t evercddl
A pre-built Docker image is available on GitHub Packages
NOTE: These Docker images only contain CBOR, CDDL and COSE. They do not contain the rest of EverParse.
The Use sections of the instructions below apply to the pre-built Docker image as well as when building by hand.
EverParse presents EverCBOR, our formally verified implementation of CBOR.
NOTE: Currently, we only support the deterministic subset of CBOR. Full support of CBOR is coming soon.
The following instructions work without F*.
EverCBOR is already built in the Docker image. If you are not using that image, you can:
-
build the C and Rust CBOR library: run
make cbor
-
test the C and Rust CBOR library: run
make cbor-test-unverified
-
C:
-
The generated C source files for CBOR are in
src/cbor/pulse/det/c
, which also contains some tests in thetest
subdirectory. There, the header file isCBORDet.h
. The object file isCBORDet.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; itsMakefile
shows how to compile and link against CBORDet.
-
-
Rust:
-
The generated Rust source files for CBOR are in
src/cbor/pulse/det/rust
, where you can usecargo build
andcargo test
; the crate is calledcborrs
. -
The generated HTML documentation of
cborrs
is athttps://project-everest.github.io/everparse/evercbor-rust/cborrs/
-
EverParse presents EverCOSign, our formally verified implementation of COSE signing.
NOTE: Support for encryption is in progress.
The following instructions work without F*.
EverCOSign is already built in the Docker image. If you are not using that image, you can:
-
build the C and Rust COSE library: run
make cose
-
test the C and Rust COSE library: run
make cose-extracted-test
- The generated C source files for COSE are in
src/cose/c
:COSE_Format.c
contains the verified parsers and serializers for COSECOSE_EverCrypt.c
is a verified implementation of sign1 and verify1 with COSE_Format and HACL* EverCryptCOSE_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) andsrc/cose/verifiedinterop/test
(HACL* EverCrypt) - The generated Rust source files for COSE are in
src/cose/rust
, where you can usecargo build
andcargo test
; the crate is calledevercosign
EverParse presents EverCDDL, our formally verified implementation of CDDL.
NOTE: We finally support table extensibility patterns such as (? 18 => int, * int => any)
.
EverCDDL is already built in the Docker image. If you are not using that image, you can build EverCDDL as follows:
-
Install opam 2.x, which you can install following the official instructions. You do not need to install OCaml, though.
-
Run
./build-evercddl.sh
. This will build EverCDDL using a local opam switch, so this will not impact your existing opam switches if 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.
We publish binary packages for EverParse as GitHub releases: https://github.com/project-everest/everparse/releases
NOTE: These binary packages do not contain CBOR, CDDL or COSE.
Full build instructions, including how to install dependencies, are available at https://project-everest.github.io/everparse/build.html, or equivalently in doc/build.rst
in this repository.
Complete TLS 1.3 message format of miTLS
Bitcoin blocks and transactions
make
./bin/qd.exe -help