everparse-asn1: Verified ASN.1 DER Parsers and Serializers

Command-line options

everparse-asn1.exe [options] main.asn [imported.asn ...]

The first file is the main module. Every module that it imports, directly or not, must also be given on the command line.

--odir DIR

The output directory (default ., created if missing).

--mname NAME

The F* module name (default: the ASN.1 module name).

--root A,B,...

The types for which to generate C functions (default: the types that no other type uses).

--keep_bytes A,B.c,...

The types (or components c of a SEQUENCE or SET B) whose parsed values keep their bytes. See KEEP-BYTES.

--lax_size_of

Accept SIZE (lo..hi) and SIZE (n) on SEQUENCE OF / SET OF, but only check that the list is non-empty when lo >= 1. The validators then accept more values than the schema allows. RFC 5280 uses such bounds, e.g. SIZE (1..ub-domain-defined-attributes).

--max_int_union N

The maximal number of values of an INTEGER constraint that is not a single range (default 256). Such a constraint is expanded into a list of values, which the validators compare in turn.

--fstar_only

Only generate the F* modules.

--skip_compilation

Do not compile the generated C code.

--fstar PATH

The F* executable. By default: $FSTAR_EXE, then the F* of the EverParse home (opt/FStar in a source tree, bin/fstar.exe in a binary package), then fstar.exe in the PATH.

--z3 PATH

The Z3 executable. By default: the one F* finds for the Z3 version of EverParse, then the one shipped with EverParse.

The EverParse home is $EVERPARSE_HOME if set, otherwise the parent of the directory of everparse-asn1.exe. The ASN.1 and LowParse libraries are taken from its lib/everparse. $CC defaults to cc.

Functions

For each root type T:

void custard_init_globals(void);  /* call once, before anything else */

bool validate_T(Pulse_Lib_Slice_slice__uint8 input, size_t *offset);

T parse_T(Pulse_Lib_Slice_slice__uint8 validated_input);

ASN1_Pulse_JitWriter_jit_result
write_T(T x, Pulse_Lib_Slice_slice__uint8 out, size_t *pos);

ASN1_Pulse_JitWriter_jit_result
write_T_typed(T x, Pulse_Lib_Slice_slice__uint8 out, size_t *pos);

A byte buffer is a slice:

typedef struct { uint8_t *elt; size_t len; } Pulse_Lib_Slice_slice__uint8;

validate_T

Checks that the bytes of input from *offset start with the DER encoding of a value of T. On success, it returns true and advances *offset past that encoding. To check that a buffer is exactly one encoding, start with *offset == 0 and check *offset == input.len afterwards.

parse_T

Must be called on validated input only: a slice of exactly the bytes accepted by validate_T. It copies nothing and allocates nothing: strings, OIDs, big INTEGERs, times and ANY values in the result are slices of the input. The result is valid as long as the input buffer is.

write_T

Writes the DER encoding of x right to left: the encoding ends at *pos, and on success *pos is moved back to its start, so the encoding is out.elt[*pos .. old *pos). Each length is written after its contents, so no size is computed beforehand. write_T returns:

• ASN1_PULSE_JITWRITER_JIT_OK: the encoding was written;

• ASN1_PULSE_JITWRITER_JIT_INVALID: x is not a valid value of T, for instance an INTEGER out of range, a string that is too long or has a forbidden character, an undeclared ENUMERATED value, or a non-minimal big INTEGER;

• ASN1_PULSE_JITWRITER_JIT_NO_SPACE: x is valid, but the encoding does not fit before *pos.

On failure, the bytes of out after *pos are unchanged. The writer also does what DER requires of the encoder: it omits a DEFAULT component equal to its default value, and sorts SET components and SET OF elements. JIT_RETRY is internal and never returned.

write_T_typed

The same C code as write_T, with a stronger F* precondition (see The Pulse API), under which it never returns JIT_INVALID.

Here is a round trip with Msg:

#include "Small.h"

int roundtrip(uint8_t *in, size_t len, uint8_t *buf, size_t buf_len) {
  custard_init_globals();
  Pulse_Lib_Slice_slice__uint8 s = { .elt = in, .len = len };
  size_t off = 0;
  if (!validate_Msg(s, &off) || off != len)
    return 1;                       /* not exactly one DER Msg */
  Msg m = parse_Msg(s);             /* zero-copy */
  Pulse_Lib_Slice_slice__uint8 o = { .elt = buf, .len = buf_len };
  size_t pos = buf_len;
  if (write_Msg(m, o, &pos) != ASN1_PULSE_JITWRITER_JIT_OK)
    return 2;
  /* buf[pos .. buf_len) == in[0 .. len) */
  return 0;
}

The complete tests are in share/everparse/tests/asn1/tool (small_test.c, x509lite_test.c, features_test.c, features2_test.c).

C types

For instance, Small.h contains:

struct Pair_s {
  int64_t left;
  Pulse_Lib_Slice_slice__uint8 right;
  Pair_note_opt note;
};

struct Msg_s {
  Msg_version_opt version;
  ASN1_Pulse_Rel_asn1_int_impl id;
  Msg_critical_opt critical;
  Msg_color_opt color;
  Alt body;
  Msg_pair_opt pair;
  LowParse_PulseParse_Iterator_Type_mixed_list__uintsize_slice_uint8 items;
  Msg_extra_opt extra;
};

KEEP-BYTES

A line --#KEEP-BYTES T in the .asn file (an ASN.1 comment, which other tools ignore), or --keep_bytes T, makes every use of T use the C type

typedef struct { T value; T_raw raw; } T_kept;

Parsers set raw (tag M_IMPL_T_RAW_PRESENT, member T_raw_present) to the slice of the input holding the DER encoding of value. This is useful to check a signature over a sub-structure, such as the tbsCertificate of an X.509 certificate. Writers ignore raw, so stale bytes are never written.

An IMPLICIT tag on T keeps the bytes too, including the new tag. --#KEEP-BYTES T.c keeps the bytes of the component c of the SEQUENCE or SET T only, including its tags.

ANY DEFINED BY tables

An ANY DEFINED BY component, or an ANY component, can be given a dispatch table in a --#DEFINED-BY comment:

--#DEFINED-BY AlgorithmIdentifier.parameters { sha256WithRSAEncryption : NULL, ecdsa-with-SHA256 : ABSENT }
--#DEFINED-BY Extension.extnValue BY extnID { id-ce-basicConstraints : CONTAINING BasicConstraints } FALLBACK NONE

Each case is ABSENT, U [OPTIONAL] or CONTAINING U. Unknown keys use the declared type of the component, the given FALLBACK U, or are rejected (FALLBACK NONE). Table constraints of information object classes (C.&Type ({Set}{@key})) are compiled to the same verified dispatch. Without a table, ANY DEFINED BY is treated as ANY.

DER encoding

The specification follows X.690 DER:

• identifiers of any class and number, in their shortest form, with a constructed bit that must match the type; definite lengths only, in their shortest form (up to \(2^{32}-1\) bytes);

• minimal INTEGER encodings; BOOLEAN TRUE encoded as 0xFF;

• OBJECT IDENTIFIER and RELATIVE-OID with minimal subidentifiers; the first OID subidentifier (40X+Y) can take several bytes;

• BIT STRING with zero padding bits;

• primitive encodings of strings (no constructed strings);

• UTCTime as YYMMDDhhmmssZ, GeneralizedTime as YYYYMMDDhhmmss[.f]Z with no trailing zero in the fraction;

• SET components sorted by tag (X.690 10.3), SET OF elements sorted by encoding (X.690 11.6);

• DEFAULT components equal to their default value are absent (X.690 11.5).

Types

• BOOLEAN, NULL, INTEGER (of any size), ENUMERATED, BIT STRING, OCTET STRING, OBJECT IDENTIFIER, RELATIVE-OID, OID-IRI, RELATIVE-OID-IRI.

• UTCTime, GeneralizedTime, DATE, TIME-OF-DAY, DATE-TIME.

• Character strings: UTF8String, PrintableString, IA5String, NumericString, VisibleString, BMPString and UniversalString, whose contents are checked; TeletexString, VideotexString, GraphicString, GeneralString and ObjectDescriptor, whose contents are not checked (see Limitations).

• SEQUENCE and SET (up to 64 components), with OPTIONAL and DEFAULT components; CHOICE; SEQUENCE OF and SET OF.

• ANY, validated as any DER value; ANY DEFINED BY.

• EXTERNAL, EMBEDDED PDV and CHARACTER STRING, through their X.680 associated types.

• OCTET STRING (CONTAINING U).

• Tags: [n], [APPLICATION n], [PRIVATE n], [UNIVERSAL n], IMPLICIT and EXPLICIT; modules with IMPLICIT, EXPLICIT or AUTOMATIC TAGS.

Constraints

• Value ranges and single values on INTEGER, with open bounds (0<..<10, MIN<..0); single values on BOOLEAN. INTEGER and ENUMERATED can have named numbers; ENUMERATED values are restricted to the declared ones.

• SIZE on OCTET STRING and character strings. SIZE counts characters: bytes, or code points for UTF8String, BMPString and UniversalString.

• SIZE (1..MAX) on SEQUENCE OF and SET OF.

• Set operations (|, UNION, ^, INTERSECTION, EXCEPT, ALL EXCEPT) and serial constraints (T (C1) (C2)), evaluated by the front end. An INTEGER constraint that is not a single range is expanded into a list of values (see --max_int_union).

• Contained subtypes (INCLUDES T) and value sets (Small INTEGER ::= { 1 | 3..5 }), which become constrained types.

• Inner type constraints: WITH COMPONENTS { ... } on SEQUENCE, SET and CHOICE, WITH COMPONENT (C) on SEQUENCE OF and SET OF.

• Extensible constraints ((0..10, ...)) are accepted and their extension is ignored, since it does not change which DER encodings are valid (X.680 49.4).

Modules, values, parameters and classes

• Type assignments and references; IMPORTS across several files.

• Value assignments of all terminal types except RELATIVE-OID (INTEGER, OBJECT IDENTIFIER such as { id-ce 19 }, BOOLEAN, strings including Quadruple and Tuple notations, '..'H / '..'B, named bits, times, IRIs), used in DEFAULT values, constraint bounds and table keys. Values of constructed types are parsed and ignored.

• DEFAULT on terminal types other than RELATIVE-OID, also under one EXPLICIT tag ([0] EXPLICIT Version DEFAULT v1) when unconstrained. F* proves by normalization that each default value is valid.

• Parameterized types (X.683) with type, value, object set and class parameters: each instance is expanded into a new type.

• Information object classes (X.681) and table constraints (X.682): CLASS with WITH SYNTAX, TYPE-IDENTIFIER, ABSTRACT-SYNTAX, objects and object sets, and components C.&Type ({Set}{@key}) with absolute or relative keys in the same SEQUENCE. An extensible object set uses the declared type for unknown keys; a non-extensible one rejects them.

Specification theorems

The specification (lib/everparse/asn1/spec) also proves:

• Conformance (ASN1.Spec.Conformance): for every well-formed schema k, the typed parser accepts an input iff the generic ANY parser accepts it with a value that conforms to k.

• Serialization (ASN1.Spec.Serializer): asn1_enc k is a total encoder, serialize_asn1 k is a LowParse serializer, and every parsed value is encodable.

• Raw values (ASN1.Spec.Raw*): constraint-free values, with check and forget between them and typed values.

Specification and library

• Not supported: REAL, extensible types (... in SEQUENCE, SET, CHOICE or ENUMERATED), recursive types, and encodings other than DER (BER, CER, PER, XER…).

• Not checked:

  • the DER rule on trailing zero bits of BIT STRINGs with named bits (X.690 11.2.2);

  • the contents of TeletexString, VideotexString, GraphicString, GeneralString and ObjectDescriptor (ISO 2022);

  • OID-IRI labels, beyond UTF-8 validity.

• Bounds: lengths are below \(2^{32}\); SIZE bounds are below 65536; SET has at most 64 components.

• SEQUENCE OF / SET OF support no SIZE constraint other than SIZE (1..MAX) (see --lax_size_of).

• SIZE constraints must be a single range; permitted alphabet (FROM) and PATTERN constraints are not supported; value sets and single values are only supported on INTEGER, ENUMERATED and BOOLEAN.

• DEFAULT is only supported on terminal types (not on SEQUENCE, SET, CHOICE, SEQUENCE OF or SET OF), and not on EXPLICIT-tagged constrained INTEGER or ENUMERATED.

• ANY cannot be a CHOICE alternative.

The everparse-asn1 front end

The front end rejects with an error the constructs listed above, and also:

• --#DEFINED-BY tables and table constraints on SET or CHOICE; with a key that is OPTIONAL, constrained or RELATIVE-OID; with a dependent component before the key; with several keys or several tables in one SEQUENCE; or with a key in another SEQUENCE than the dependent component.

• KEEP-BYTES on a CHOICE alternative, on a DEFAULT component, or on the key and dependent components of a DEFINED-BY table. A CHOICE alternative of a KEEP-BYTES type does not keep its bytes (with a warning).

• Information object classes beyond type fields selected by a key: value fields selected by a key, value set, object and object set fields, variable-type value fields, parameterized object sets, and DEFAULT on a dependent component. Two objects with the same UNIQUE key are not reported (the first one wins).

• Parameterized values, value sets, objects and object sets; recursive parameterized instances.

• ENCODED BY with an encoding other than DER.

• Ambiguous schemas are reported by F* (seq_tac / set_tac), not by the front end.

C API

• No C iterator is generated for parsed SEQUENCE OF / SET OF lists: the caller walks the payload, which is a sequence of validated TLVs.

• validate_T, parse_T and the writers are only generated for root types (--root).

• The names of the generic C types, such as Pulse_Lib_Slice_slice__uint8, are generated by Custard and may change across versions.

• No per-type introduction lemmas are generated for the writer relation raw_varel: a verified Pulse caller of write_T has to unfold it.