3d: Dependent Data Descriptions for Verified Validation¶
The documentation from this page covers the EverParse/3d releases v2021.03.05 or later. Documentations for earlier versions may be found in the Git history.
EverParse/3d lets you write a data format description and automatically produces efficient data validation code formally verified for memory-safety (absence of buffer overruns), functional correctness (validation is correct wrt. your data format) and security (absence of double memory fetches.) A gentle overview of formal verification is available in the documentation of EverCrypt; EverParse provides similar formal guarantees except secret-independence.
- Write your data format description in the 3d language, as
- Give MyFile1.3d and MyFile2.3d to EverParse:
- with the Windows binary package:
everparse.cmd MyFile1.3d MyFile2.3d
- with the Linux binary package:
everparse.sh MyFile1.3d MyFile2.3d
- with the source tree:
bin/3d.exe --batch MyFile1.3d MyFile2.3d
- with the Windows binary package:
Then, EverParse/3d produces:
MyFile1.fst: the verified F* specification and Low* implementation of parsers and validators for your data format from
MyFile1.3d, and similarly for
MyFile1.h: the verified C code generated from the verified F* and Low* files, and similarly for
MyFile1Wrapper.h: an entrypoint API to call into the verified C code, and similarly for
EverParseEndianness.h: various EverParse helpers for the implementation of verified validators, common to
#include "MyFile1Wrapper.h"into any of your C compilation units that need to call a validator from
MyFile1.3d, and similarly for
For each message type in the source data formats, the generated C code provides a _validator_, a procedure to determine if a given input array of bytes contains a valid representation of a message, with the following properties:
- Memory safety: The validator is memory safe, meaning it never accesses memory out of bounds, accesses memory at an incompatible type, uses memory after it has been freed, etc.
- Arithmetic safety: The validator has no integer overflows or underflows.
- Double-fetch freedom: The validator reads every byte in the input array at most once, defending against certain kinds of time-of-check/time-of-use bugs.
- Write footprint: The validator does not modify the input array, and only modifies memory as described by user-controlled imperative actions that are explicit in the specification.
- No heap allocation: The validator does not allocate any memory on the heap.
- Functionally correct: The validator accepts all input arrays that contain valid representations of the message according to its specification, rejecting all others.
Download and install¶
We provide binary (x86_64 only) packages for Windows and Linux.
- Download the binary package corresponding to your platform, from the latest EverParse/3d release.
- Extract it (Windows:
tar xzf) anywhere you like. No need to configure it anyhow.
Then, everything is contained in a
everparse directory, whose
actual entrypoint executable is
everparse.cmd (for Windows) or
everparse.sh (for Linux.)
Binary packages already contain all dependencies required by EverParse, such as F*, KaRaMeL and z3, so no need to install anything beforehand.
The Windows binary package contains a binary snapshot of clang-format to pretty-print the produced
.h files. On Linux, you may want to install clang-format (more
info at the LLVM download page), but this is optional.
The Windows binary package is fully native, in the sense that it does not require any POSIX emulation layer such as Cygwin or WSL.
everparse.cmd [options] input_files
everparse.sh [options] input_files
From the source tree:
bin/3d.exe. Caveat: in that case, no options
are toggled by default (not even
and you need to provide all options by hand.
Options are treated from left to right:
Tell EverParse to write all files to the directory
output_directory_name. This directory must already exist (EverParse will not create it.) The default is
Verify the produced F*
.fstifiles and generate C
.hfiles. This is toggled by default.
Do not verify the produced F*
.fstifiles or generate C
clang-formaton extracted .c/.h files. This option automatically toggles
This is toggled by default on Windows, since the Windows binary package contains a copy of clang-format. On Linux, this is toggled by default only if
clang-formatis reachable through the
Do not call clang-format on extracted .c/.h files.
Provide the path to clang-format if not reachable through
PATH(or to override the one provided in the Windows binary package.) This option automatically toggles
--batch, remove all produced intermediate files other than
.h` files (thus: ``.fst,
Keep all produced intermediate files. This is toggled by default.
Options are treated from left to right, with higher priority on
right-most options. Thus, any
--no_clang_format will override any
its left, and vice-versa.
You can provide one or more
input_files to EverParse. Then,
EverParseEndianness.h will be shared across
.h files produced for all the
.3d files that you
EverParse input files must all bear the
.3d file name extension,
and their names must start with a capital letter.
Alternate mode: generating a Makefile¶
By default, with
--batch, given a
.3d specification, EverParse
.h files by first producing
.fst files files containing verified F* specifications and
implementations of validators, and then calling F* and KaRaMeL on each
such file to verify and extract them to C. EverParse will issue all
such calls to F* and KaRaMeL sequentially.
everparse.cmd --makefile gmake Test.3d (on
./everparse.sh on Linux), instead of producing
.h files, EverParse will take
Test.3d and all of the
modules it depends on, and produce a GNU Makefile containing all
recipes and rules to produce
.h files and all
intermediate files with proper dependencies so that the user can
leverage GNU Make parallelism for any rules that do not depend on one
another. Other build systems are supported with variations of the
--makefile option, as stated below.
The produced Makefile will make use of three variables:
EVERPARSE_CMD: the command to run EverParse. This variable must contain the path and name of the EverParse executable, and any options (
--clang_format, etc.) useful to produce .
EVERPARSE_INPUT_DIR: the path to the input files.
.3d files must be located in the same input
EVERPARSE_OUTPUT_DIR: the path to the output files. EverParse will append the
CC: the path and name of the C compiler that will be used to compile the produced C files.
CFLAGS: options to provide to the C compiler to compile the produced C files.
The produced Makefile, by default called
meant to be included in the main
Makefile of your project. On
Linux, such a typical main
Makefile for use with GNU Make may look
all: test EVERPARSE_CMD=/path/to/everparse.sh EVERPARSE_OUTPUT_DIR=obj EVERPARSE_INPUT_DIR=src everparse_makefile=$(EVERPARSE_OUTPUT_DIR)/EverParse.Makefile source_files=$(wildcard $(EVERPARSE_INPUT_DIR)/*.3d) $(EVERPARSE_OUTPUT_DIR): mkdir -p $@ $(everparse_makefile): $(source_files) $(EVERPARSE_OUTPUT_DIR) $(EVERPARSE_CMD) --makefile gmake --makefile_name $@ $(source_files) include $(everparse_makefile) test: $(EVERPARSE_ALL_O_FILES) clean: rm -rf $(EVERPARSE_OUTPUT_DIR) .PHONY: all test clean
A fully commented version of that main
Makefile is available in
the EverParse repository.
EverParse supports the following command-line options relevant to this mode:
--makefile gmake: produce a Makefile for use with GNU Make.
--makefile nmake: produce a Makefile for use with Microsoft NMAKE.
--makefile_name my_file_name: the name of the produced Makefile shall be
my_file_nameinstead of the default
--skip_o_rules: do not output rules that would produce
.ofiles by compiling
Alternate mode: hash checking¶
To speed up some scenarios where the user maintains a snapshot of the
generated .c and .h files to skip unnecessary verification time when
.3d files are not changed, EverParse provides an optional mechanism to
record the hash of .3d, .c and .h files and to compare them to skip
reverification and regeneration. This mechanism is disabled by
default, and has to be explicitly enabled using the
option as described below. WARNING: this mode will weaken
verification guarantees to the probability of hash collisions!
If enabled, then EverParse checks the hashes of the .3d and maybe .c and .h files (depending on the variant, as described below) and fails if hashes do not match; no verification or regeneration is performed at all.
Hashes are computed and checked using the EverCrypt verified cryptographic library, which is included in EverParse binary packages.
Options relevant to this mode:
--save_hashes: save the hashes of the contents of source .3d, .c and .h files into a .json file. This option can be added in default mode when generating .c and .h files.
--check_hashes strong: checks the hashes of the contents of source .3d, .c and .h files, by reading the recorded hash from the .json file created by
--check_hashes weak: checks the hashes of the contents of source .3d files only, by reading the recorded hash from the .json file created by
--save_hashes, leaving the option for the user to manually change the generated .c and .h files (WARNING: this will void all verification guarantees!)
--check_hashes inplace: same as
--check_hashes weak, but uses the hash recorded in the copyright header of the generated .c and .h files instead of the .json file. The hash is introduced by using the
EVERPARSEHASHESkeyword in the corresponding
.copyright.txtused to prepend generated .c and .h files with copyright headers; see Copyright headers for more details.
--check_inplace_hash MyFile.3d=MyFile.h: same as
--check_hashes inplace, but instead manually specifies the pair of the source
.3dfile and the already-generated
.c) file in which to check the hash. This option can be specified several times to provide several such pairs to check.
Alternate mode: help and version¶
Some options make EverParse do nothing other than show a help or version message:
Print the version of EverParse/3d and exit (do not process any further options to the right, nor any files at all.)
Show the usage message and the status of some options given so far, and exit (do not process any further options to the right, nor any files at all.)