3d: Dependent Data Descriptions for Verified Validation

Formal guarantees

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.

Default mode

In default mode, EverParse3d produces C code corresponding to validators proven correct with respect to the 3d specification.

Options are treated from left to right:

• --odir output_directory_name

  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 . (current directory)

• --batch

  Verify the produced F* .fst and .fsti files and generate C .c and .h files. This is toggled by default.

• --no_batch

  Do not verify the produced F* .fst and .fsti files or generate C .c and .h files.

• --clang_format

  Call clang-format on extracted .c/.h files. This option automatically toggles --batch.

  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-format is reachable through the PATH environment variable.

• --no_clang_format

  Do not call clang-format on extracted .c/.h files.

• --clang_format_executable

  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 --clang_format and --batch.

• --clang_format_use_custom_config

  With --clang_format, skip copying the .clang-format file from the EverParse distribution, and assume that there is already an existing .clang-format

• --cleanup

  With --batch, remove all produced intermediate files other than .c and .h` files (thus: ``.fst, .fsti, .checked, .krml)

• --no_cleanup

  Keep all produced intermediate files. This is toggled by default.

• --skip_c_makefiles

  Skip generating the default Makefiles produced by Karamel to compile the produced C code.

• --add_include <myinclude.h>

  --add_include "myinclude.h"

  Prepend each produced C file with a #include <myinclude.h> or a #include "myinclude.h" C preprocessor directive.

• --config myfile.config

  Use the specified JSON file myfile.config to declare compile-time flags (see compile-time configuration in the 3D language reference.)

• --json

  Print the abstract syntax tree of each input .3d file, as it stands after name resolution and type-checking, to standard output as a JSON value, one per line. This is a debugging aid: the encoding follows the shape of the 3d abstract syntax rather than any documented schema, and it is not stable across EverParse versions.

  A constructor is encoded as an array whose first element is the constructor name followed by one element per argument, so a constructor with no argument is a one-element array; a record is encoded as an object keyed by the field names; None is null and Some x is the encoding of x. Source locations and comments are omitted.

• --fstar path/to/fstar.exe

  Allows to specify the location of the F* executable. The everparse.sh / everparse.cmd script in the EverParse binary package is already configured to use the F* executable provided in the package. Otherwise, the default is to use the fstar.exe found from the PATH.

• --api pulse|lowstar

  Selects the public C API. Both are implemented with the verified Pulse backend. Shared named error kinds use the same numbers in both APIs.

  lowstar is the default; explicitly selecting it is equivalent to omitting --api. It uses Pulse validators behind verified compatibility adapters, preserving the original Low* public C API: scalar buffer positions, packed 64-bit validator results, error callbacks, copy-buffer projections, and buffer, extern and static input primitives. Existing Low* C clients need no signature changes. Private workers still use byte-sized statuses and mutable cursors; they are not part of the public API. Its self-contained EverParse.h is generated from the Pulse library in lib/everparse/3d/krml/lowstar/<backend>/. It includes both the public packed-result helpers and separately named internal byte-status helpers; no separate EverParsePulseInternal.h is needed. During per-parser extraction, KaRaMeL uses the shipped runtime without emitting another EverParse.h. With --no_copy_everparse_h, supply this header, not the one used by --api pulse; see --no_copy_everparse_h below for the runtime directory matching each selection.

  pulse exposes the native Pulse API. See the Pulse backend primitives part of --input_stream below, and, in the 3d language reference, Error handling under --api pulse and Probing under --api pulse.

  This replaces the former --pulse switch, which is no longer accepted. --no_api resets the selection to lowstar. API selection is independent of --input_stream: both APIs support buffer, extern and static, subject to the native Pulse probe restriction.

  Generated Makefile commands retain the selected API, and hash checks distinguish the two APIs.

  The Low*-API test corpus lives in share/everparse/tests/3d/lowstar. Its ordinary builds explicitly select --api lowstar. share/everparse/tests/3d/pulse-lowstar-diff compares the Low*-compatible and native Pulse APIs, including wrapper returns, outparameters, copy buffers, and callback diagnostics. It is also part of make 3d-test on Pulse-enabled Linux builds.

• --complete_wrappers

  For each entrypoint, generate a second wrapper that additionally checks that the validator consumed the whole input buffer.

  By default, the <Mod>Check<Typ>(base, len) wrapper recognizes a prefix: it returns TRUE as soon as base starts with valid <Typ> data fitting within len bytes, and says nothing about the bytes that follow. For instance, the point entrypoint of the HelloWorld.3d of the 3d language reference is two UINT16s, hence 4 bytes wide, so HelloWorldCheckPoint(base, 5) returns TRUE on any buffer whose first 4 bytes are a valid point, whatever the fifth byte is. This is deliberate – a message is routinely read into a fixed-size buffer larger than itself, and the underlying verified validator reports how many bytes it consumed, which is what lets an enclosing format resume parsing after the message – but it is not what a caller validating a standalone message wants.

  With --complete_wrappers, the usual wrapper keeps that behavior, and 3d emits alongside it a second one, with Complete in its name and the same signature, that returns TRUE only if validation succeeded and consumed exactly len bytes. On trailing bytes it calls <Mod>EverParseError with the type name, an empty field name, and "unexpected trailing bytes" as the reason, then returns FALSE. So, for that point entrypoint:

  BOOLEAN HelloWorldCheckPoint(uint8_t *base, uint32_t len);
  BOOLEAN HelloWorldCheckCompletePoint(uint8_t *base, uint32_t len);
  

  The naming rule, the behavior of probe entrypoints, and the treatment of user-named entrypoints (whose complete-check counterpart is the given name suffixed with Complete) are described in the 3d language reference.

  This option works with both --api selections. It is, however, only meaningful with --input_stream buffer (the default): with extern or static the wrapper is handed an opaque stream rather than a byte array and a length, so it has no notion of the end of the input, and the option has no effect.

  Both wrappers are unverified glue code, generated into <Mod>Wrapper.c; the formal guarantees listed above are those of the <Mod>Validate<Typ> validator that they call.

• --no_complete_wrappers

  Generate only the plain entrypoint wrappers. This is toggled by default.

• --input_stream buffer|extern|static

  Specifies the format of validator input buffers:

  • With buffer (which is the default), a validator takes as argument a byte array and its length.

  • With extern, a validator takes as argument a value of a user-defined EVERPARSE_INPUT_STREAM_BASE type, representing an input byte stream. The client must define that type, and a set of functions over it that depends on the selected API: --api lowstar (the default) and --api pulse use different names and argument types. Both sets are given below.

    Low*-compatible primitives (--api lowstar)

    extern BOOLEAN EverParseHas(
      EVERPARSE_EXTRA_T _extra_t,
      EVERPARSE_INPUT_STREAM_BASE x,
      uint64_t n
    );
    

    EverParseHas returns 1 if the input stream x has n bytes available to read, 0 otherwise.

    extern uint8_t* EverParseRead(
      EVERPARSE_EXTRA_T _extra_t,
      EVERPARSE_INPUT_STREAM_BASE x,
      uint64_t n,
      uint8_t *dst
    );
    

    EverParseRead takes and reads n bytes from the input stream x, possibly copying them into dst, and returns a byte array containing the bytes read. There is no requirement that the function returns dst, or even that a copy to dst is made.

    extern void EverParseSkip(
      EVERPARSE_EXTRA_T _extra_t,
      EVERPARSE_INPUT_STREAM_BASE x,
      uint64_t n
    );
    

    EverParseSkip advances the input stream x by n bytes without reading them.

    extern uint8_t* EverParsePeep(
      EVERPARSE_EXTRA_T _extra_t,
      EVERPARSE_INPUT_STREAM_BASE x,
      uint64_t n
    );
    

    EverParsePeep returns a pointer to a byte array that is part of the input stream x and points to its next n bytes, then advances the input stream by n. If such operation is impossible, then returns NULL. Such a pointer is returned by the field_ptr_after action (see “Atomic actions” in the 3d language reference), so it is the responsibility of the application to ensure double-fetch freedom on the contents of the returned field is preserved.

    extern uint64_t EverParseEmpty(
      EVERPARSE_EXTRA_T _extra_t,
      EVERPARSE_INPUT_STREAM_BASE x
    );
    

    EverParseEmpty skips to the end of the input stream x and returns the number of bytes so skipped, without reading them.

    In all such functions, EVERPARSE_EXTRA_T is a user-defined type for the context used for error handling (see “Error handling” in the 3d language reference.)

    Pulse backend primitives (with --api pulse)

    With --api pulse, none of the primitives above are used. The extern and static input streams instead require the following set. Except for EverParseStreamGetPosition, each receives the EVERPARSE_EXTRA_T context that was passed to the validator, but byte counts are size_t rather than uint64_t:

    extern uint64_t EverParseStreamGetPosition(EVERPARSE_INPUT_STREAM_BASE base);
    extern BOOLEAN EverParseStreamHas        (EVERPARSE_EXTRA_T extra, EVERPARSE_INPUT_STREAM_BASE base, size_t n);
    extern BOOLEAN EverParseStreamHasAt      (EVERPARSE_EXTRA_T extra, EVERPARSE_INPUT_STREAM_BASE base, size_t off, size_t n);
    extern void    EverParseStreamReadBytes  (EVERPARSE_EXTRA_T extra, EVERPARSE_INPUT_STREAM_BASE base, size_t n, uint8_t *dst);
    extern void    EverParseStreamSkip       (EVERPARSE_EXTRA_T extra, EVERPARSE_INPUT_STREAM_BASE base, size_t n);
    extern size_t  EverParseStreamEmpty      (EVERPARSE_EXTRA_T extra, EVERPARSE_INPUT_STREAM_BASE base);
    
    /* only if the grammar uses the `field_ptr_after` action */
    extern BOOLEAN  EverParseFieldPtrAfterImpl(EVERPARSE_EXTRA_T extra, uint64_t sz, uint8_t **w,
                                               EVERPARSE_INPUT_STREAM_BASE base);
    extern uint8_t *EverParseNullPtr;
    

    With --input_stream static, every one of these is declared static inline rather than extern, except EverParseNullPtr; see the static bullet below. share/everparse/tests/3d/static is a worked example, and the EverParse.h that --api pulse copies into the output directory is the authoritative declaration of this set.

    EverParseStreamGetPosition(base) returns the absolute position of the stream, that is, the total number of bytes it has consumed since it was created. The generated wrapper samples it on both sides of the validator call and subtracts the two, to recover the parsed size; it must therefore be cumulative, and in particular must keep counting across successive validations on the same stream. It is the one primitive whose signature has no EVERPARSE_EXTRA_T parameter; besides being used inside the validators, it is called directly from the generated <Mod>Wrapper.c.

    EverParseStreamHas(extra, base, n) returns TRUE iff n bytes are available at the current position, and must consume nothing.

    EverParseStreamHasAt(extra, base, off, n) returns TRUE iff n bytes are available starting off bytes after the current position, and must consume nothing. Unlike EverParseStreamGetPosition’s result, off is relative; an implementation that treats it as an absolute offset will read out of bounds and accept truncated input, since this call is the entire bounds check performed by the non-consuming validators. The validators never ask about an off beyond the end of the stream, so the answer in that case is unspecified – but the implementation must still reach it safely, in particular by guarding against off + n overflowing.

    EverParseStreamReadBytes(extra, base, n, dst) copies the next n bytes of the stream into dst and advances the stream by n. It is only ever called to read a leaf integer, so n is at most 8.

    EverParseStreamSkip(extra, base, n) advances the stream by n bytes without reading them.

    EverParseStreamEmpty(extra, base) returns the number of bytes remaining and consumes all of them; it backs all_bytes. It is only ever called on an unbounded stream: within a size-bounded field such as t_at_most, the generated code instead computes what the bound says is left and drains it with EverParseStreamSkip, so that the bytes following the bounded region are not swallowed.

    EverParseFieldPtrAfterImpl(extra, sz, w, base) backs the field_ptr_after action, which the buffer input stream does not have. It should store into *w a pointer to the next sz bytes of the stream, advance the stream by sz, and return TRUE; if it cannot, it must return FALSE and leave *w alone, in which case the generated code reports a failure. Its F* specification constrains neither the pointer written nor the stream, so – exactly as for EverParsePeep under --api lowstar – it is the responsibility of the application to ensure double-fetch freedom on the contents of the returned field is preserved. EverParseNullPtr is the value the generated code stores into *w before the call.

    Finally, and exactly as in the Low*-compatible API, the client supplies the two wrapper-level callbacks below. These are common to both APIs:

    extern void EverParseHandleError(EVERPARSE_EXTRA_T extra, uint64_t parsedSize,
                                     const char *typename, const char *fieldname,
                                     const char *reason, uint64_t error_code);
    extern void EverParseRetreat    (EVERPARSE_EXTRA_T extra, EVERPARSE_INPUT_STREAM_BASE base,
                                     uint64_t parsedSize);
    

    EverParseHandleError is the error callback described under “Error handling” in the 3d language reference. EverParseRetreat is called by the generated wrapper on the way out, with the number of bytes the validator consumed; a client that makes it genuinely rewind the stream must nevertheless not let it rewind EverParseStreamGetPosition, on which the wrapper’s arithmetic depends.

    Three differences from the Low*-compatible contract of --api lowstar are worth calling out when porting a client:

    • The stream tracks its own position. The generated <Mod>Check<Type> wrapper has the same signature as under --api lowstar, but the Pulse validator it calls returns a plain uint8_t error code rather than a packed uint64_t, so the wrapper cannot read the parsed size out of the result. It recovers that size by sampling EverParseStreamGetPosition on either side of the call and subtracting – which is why that primitive has to be cumulative.

    • Reads always copy. EverParseStreamReadBytes returns void, so, unlike EverParseRead, it cannot hand back a pointer into the client’s own storage.

    • There is no EverParsePeep. The field_ptr action is restricted to the buffer input stream under both APIs, so nothing is lost there; but field_ptr_after is backed by the explicit EverParseFieldPtrAfterImpl primitive above rather than by EverParsePeep, and it needs EverParseNullPtr as well.

  • static is like extern except that the functions on EVERPARSE_INPUT_STREAM_BASE are declared static inline rather than extern, so that the compiler sees each stream operation at every validator call site instead of linking against it. This holds for both APIs. The client must therefore define those functions, not merely implement them in a separate translation unit: the header named by --input_stream_include is included into every generated .c file, so that is where the definitions belong. Under --api pulse, EverParseNullPtr is the exception – it is a value, not a function, and stays extern under both input streams.

  By default, 3d copies the matching EverParse.h and supporting headers into the output directory for both APIs. Add that directory to the C include path. With --no_copy_everparse_h, instead use the runtime directory matching both --api and --input_stream:

  • lowstar: lib/everparse/3d/krml/lowstar/<input_stream_format>

  • pulse: lib/everparse/3d/krml/<input_stream_format>

  These paths are relative to the EverParse package or repository. Also include src/3d for the supporting headers. Despite preserving the Low* public C API, --api lowstar needs its own runtime header, not the Pulse one.

• --input_stream_include myinclude.h

  With --input_stream, defines the name of the C include file that provides definitions for EVERPARSE_INPUT_STREAM_BASE and its associated functions.

Alternate mode: generating a Makefile

By default, with --batch, given a .3d specification, EverParse produces .c and .h files by first producing .fsti and .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.

Alternatively, with everparse.cmd --makefile gmake Test.3d (on Windows; use ./everparse.sh on Linux), instead of producing .c and .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 .c and .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.

• EVERPARSE_OUTPUT_DIR: the path to the output files. EverParse will append the --odir option appropriately.

• 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 EverParse.Makefile, is 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 like:

Also valid in Makefile generation mode are the following options:

• --clang_format

  Add .clang-format as a dependency of generated .c and .h files, and produce a rule to generate .clang-format

• --clang_format_use_custom_config

  Same as --clang_format, but do not produce a rule to generate .clang-format

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_name instead of the default EverParse.Makefile.

• --skip_o_rules: do not output rules that would produce .o files by compiling .c files.

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 --check_hashes 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 --save_hashes.

• --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 EVERPARSEHASHES keyword in the corresponding .copyright.txt used 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 .3d file and the already-generated .h (or .c) file in which to check the hash. This option can be specified several times to provide several such pairs to check.

Alternate mode: test case generation

Given a 3d specification, EverParse can now generate positive (resp. negative) test cases. Internally, EverParse converts the 3d specification into a SMT2 theory, and then asks Z3 for the following satisfiability question: is there any sequence of bytes passing (resp. failing) the parser specification?

The following options are mutually exclusive:

• --z3_test MyModule.my_parser

  (requires MyModule.3d to be specified on the command line) produces positive and negative test cases for my_parser defined in MyModule.3d .

  This option produces the following results:

  • a series of binary files containing the contents of each test case. Each binary file is named as follows:

    witness.n.POS.i.validatorname.args.dat

    where:

    • n is the test case number

    • POS (resp. NEG) indicates a positive (resp. negative) test case

    • i is a probe counter: 0 corresponds to the input buffer passed to the validator; a positive value corresponds to the i-th time a probe 3d construct is encountered. (If the 3d specification contains no probe construct, then only the 0 file will be created for each test case.)

      More precisely, when encountering a T *ptr probe ProbeFunction(length = ..., destination = ...) pointer field, the binary contents for that field in a test case is the big-endian representation of a positive 64-bit integer i so that the contents of the file with probe index i is meant to be passed to the validator for T.

    • validatorname is the name of the validator function produced by EverParse. It has the shape ModuleValidateMyParser

    • args is the sequence of the non-outparameter argument values passed to the validator, separated by . ; all of those argument values are integers.

  • a C test program, testcases.c, that produces C definitions of the test cases, and calls to the validator with those test cases.

    A given test case is an array of layers; a layer is a byte array and its length. Layer 0 contains the byte array passed to the validator; layer of a positive index i contains the byte array passed to the validator corresponding to the i-th time a probe pointer field is encountered.

  • with --batch (set by default when using the everparse.sh / everparse.bat script from the binary package), this option also compiles the C test program into test.exe and runs it to check whether the generated test cases are actually accepted or rejected by the verified validator implementations for the given 3d parser specifications. Then, the test program prints on standard output the C definitions of the test cases.

    Use --no_batch to disable compilation of the C test program.

• --z3_diff_test MyModule1.my_parser1,MyModule2.my_parser2

  (requires MyModule1.3d and MyModule2.3d to be specified on the command line) produces a set of test cases that are positive for my_parser1 but negative for my_parser2, and a set of test cases for the converse.

  The shape of the produced results is similar to those produced by --z3_test (see above), except that the test file name also contains the name of the second validator against which it is negative.

• --emit_smt_encoding

  produces the SMT2 encoding corresponding to the .3d files passed as argument. Such encoding is printed on standard output.

• --test_checker MyModule.my_parser

  (requires MyModule.3d to be specified on the command line) produces a test checker executable for the given parser, test.exe. The test checker takes as arguments:

  • a binary file name containing the contents of the input buffer to be passed to the validator

  • the non-outparameter integer argument values to be passed to the validator

  The test checker executable returns exit code:

  • 0 if validation succeeds and consumes all input bytes

  • 1 if validation succeeds but the validator does not consume all input bytes

  • 2 if validation fails

  • 3 if the input file is larger than 4 GB, or if any system error occurs (file does not exist, read error, etc.)

  Note

  The test checker executable currently does not work with 3d specifications containing probes.

Alternate mode: help and version

Some options make EverParse do nothing other than show a help or version message:

• --version

  Print the version of EverParse/3d and exit (do not process any further options to the right, nor any files at all.)

• --help

  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.)