OCaml-TLS: ASN.1 and notation embedding

This is the fourth in a series of posts that introduce new libraries for a pure OCaml implementation of TLS. You might like to begin with the introduction.

asn1-combinators is a library that allows one to express ASN.1 grammars directly in OCaml, manipulate them as first-class entities, combine them with one of several ASN encoding rules and use the result to parse or serialize values.

It is the parsing and serialization backend for our X.509 certificate library, which in turn provides certificate handling for ocaml-tls. We wrote about the X.509 certificate handling yesterday.

What is ASN.1, really?

ASN.1 (Abstract Syntax Notation, version one) is a way to describe on-the-wire representation of messages. It is split into two components: a way to describe the content of a message, i.e. a notation for its abstract syntax, and a series of standard encoding rules that define the exact byte representations of those syntaxes. It is defined in ITU-T standards X.680-X.683 and X.690-X.695.

The notation itself contains primitive grammar elements, such as BIT STRING or GeneralizedTime, and constructs that allow for creation of compound grammars from other grammars, like SEQUENCE. The notation is probably best introduced through a real-world example:

-- Simple name bindings
UniqueIdentifier ::= BIT STRING

-- Products
Validity ::= SEQUENCE {
  notBefore Time,
  notAfter  Time
}

-- Sums
Time ::= CHOICE {
  utcTime     UTCTime,
  generalTime GeneralizedTime
}

(Example from RFC 5280, the RFC that describes X.509 certificates which heavily rely on ASN.)

The first definition shows that we can introduce an alias for any existing ASN grammar fragment, in this case the primitive BIT STRING. The second and third definitions are, at least morally, a product and a sum.

At their very core, ASN grammars look roughly like algebraic data types, with a range of pre-defined primitive grammar fragments like BIT STRING, INTEGER, NULL, BOOLEAN or even GeneralizedTime, and a number of combining constructs that can be understood as denoting sums and products.

Definitions such as the above are arranged into named modules. The standard even provides for some abstractive capabilities: initially just a macro facility, and later a form of parameterized interfaces.

To facilitate actual message transfer, a grammar needs to be coupled with an encoding. By far the most relevant ones are Basic Encoding Rules (BER) and Distinguished Encoding Rules (DER), although other encodings exist.

BER and DER are tag-length-value (TLV) encodings, meaning that every value is encoded as a triplet containing a tag that gives the interpretation of its contents, a length field, and the actual contents which can in turn contain other TLV triplets.

Let's drop the time from the example above, as time encoding is a little involved, and assume a simpler version for a moment:

Pair ::= SEQUENCE {
  car Value,
  cdr Value
}

Value ::= CHOICE {
  v_str UTF8String,
  v_int INTEGER
}

Then two possible BER encodings of a Pair ("foo", 42) are:

  30         - SEQUENCE            30         - SEQUENCE
  08         - length              0c         - length
  [ 0c       - UTF8String          [ 2c       - UTF8String, compound
    03       - length                07       - length
    [ 66     - 'f'                   [ 0c     - UTF8String
      6f     - 'o'                     01     - length
      6f ]   - 'o'                     [ 66 ] - 'f'
    02       - INTEGER                 0c     - UTF8String
    01       - length                  02     - length
    [ 2a ] ] - 42                      [ 6f   - 'o'
                                         6f ] - 'o'
                                     02       - INTEGER
                                     01       - length
                                     [ 2a ] ] - 42

The left one is also the only valid DER encoding of this value: BER allows certain freedoms in encoding, while DER is just a BER subset without those freedoms. The property of DER that any value has exactly one encoding is useful, for example, when trying to digitally sign a value.

If this piqued your curiosity about ASN, you might want to take a detour and check out this excellent writeup.

A bit of history

The description above paints a picture of a technology a little like Google's Protocol Buffers or Apache Thrift: a way to declaratively specify the structure of a set of values and derive parsers and serializers, with the addition of multiple concrete representations.

But the devil is in the detail. For instance, the examples above intentionally gloss over the fact that often concrete tag values leak into the grammar specifications for various disambiguation reasons. And ASN has more than 10 different string types, most of which use long-obsolete character encodings. Not to mention that the full standard is close to 200 pages of relatively dense language and quite difficult to follow. In general, ASN seems to have too many features for the relatively simple task it is solving, and its specification has evolved over decades, apparently trying to address various other semi-related problems, such as providing a general Interface Description Language.

Which is to say, ASN is probably not what you are looking for. So why implement it?

Developed in the context of the telecom industry around 30 years ago, modified several times after that and apparently suffering from a lack of a coherent goal, by the early 90s ASN was still probably the only universal, machine- and architecture-independent external data representation.

So it came easily to hand around the time RSA Security started publishing its series of PKCS standards, aimed at the standardization of cryptographic material exchange. RSA keys and digital signatures are often exchanged ASN-encoded.

At roughly the same time, ITU-T started publishing the X.500 series of standards which aimed to provide a comprehensive directory service. Much of this work ended up as LDAP, but one little bit stands out in particular: the X.509 PKI certificate.

So a few years later, when Netscape tried to build an authenticated and confidential layer to tunnel HTTP through, they based it on -- amongst other things -- X.509 certificates. Their work went through several revisions as SSL and was finally standardized as TLS. Modern TLS still requires X.509.

Thus, even though TLS uses ASN only for encoding certificates (and the odd PKCS1 signature), every implementation needs to know how to deal with ASN. In fact, many other general cryptographic libraries also need to deal with ASN, as various PKCS standards mandate ASN as the encoding for exchange of cryptographic material.

The grammar of the grammar

As its name implies, ASN was meant to be used with a specialized compiler. ASN is really a standard for writing down abstract syntaxes, and ASN compilers provided with the target encoding will generate code in your programming language of choice that, when invoked, parses to or serializes from ASN.

As long as your programming language of choice is C, C++, Java or C#, obviously -- there doesn't seem to be one freely available that targets OCaml. In any case, generating code for such a high-level language feels wrong somehow. In its effort to be language-neutral, ASN needs to deal with things like modules, abstraction and composition. At this point, most functional programmers reading this are screaming: "I already have a language that can deal with modules, abstraction and composition perfectly well!"

So we're left with implementing ASN in OCaml.

One strategy is to provide utility functions for parsing elements of ASN and simply invoke them in the appropriate order, as imposed by the target grammar. This amounts to hand-writing the parser and is what TLS libraries in C typically do.

As of release 1.3.7, PolarSSL includes ~7,500 lines of rather beautifully written C, that implement a specialized parser for dealing with X.509. OpenSSL's libcrypto contains ~50,000 lines of C in its 'asn1', 'x509' and 'x509v3' directories, and primarily deals with X.509 specifically as required by TLS.

In both cases, low-level control flow is intertwined with the parsing logic and, above the ASN parsing level, the code that deals with interpreting the ASN structure is not particularly concise. It is certainly a far cry from the (relatively) simple grammar description ASN itself provides.

Since in BER every value fully describes itself, another strategy is to parse the input stream without reference to the grammar. This produces a value that belongs to the general type of all ASN-encoded trees, after which we need to process the structure according to the grammar. This is similar to a common treatment of JSON or XML, where one decouples parsing of bytes from the higher-level concerns about the actual structure contained therein. The problem here is that either the downstream client of such a parser needs to constantly re-check whether the parts of the structure it's interacting with are really formed according to the grammar (probably leading to a tedium of pattern-matches), or we have to turn around and solve the parsing problem again, mapping the uni-typed contents of a message to the actual, statically known structure we require the message to have.

Surely we can do better?

LAMBDA: The Ultimate Declarative

Again, ASN is a language with a number of built-in primitives, a few combining constructs, (recursive) name-binding and a module system. Our target language is a language with a perfectly good module system and it can certainly express combining constructs. It includes an abstraction mechanism arguably far simpler and easier to use than those of ASN, namely, functions. And the OCaml compilers can already parse OCaml sources. So why not just reuse this machinery?

The idea is familiar. Creating embedded languages for highly declarative descriptions within narrowly defined problem spaces is the staple of functional programming. In particular, combinatory parsing has been known, studied and used for decades.

However, we also have to diverge from traditional parser combinators in two major ways. Firstly, a single grammar expression needs to be able to generate different concrete parsers, corresponding to different ASN encodings. More importantly, we desire our grammar descriptions to act bidirectionally, producing both parsers and complementary deserializers.

The second point severely restricts the signatures we can support. The usual monadic parsers are off the table because the expression such as:

( (pa : a t) >>= fun (a : a) ->
  (pb : b t) >>= fun (b : b) ->
  return (b, b, a) ) : (b * b * a) t

... "hides" parts of the parser inside the closures, especially the method of mapping the parsed values into the output values, and can not be run "in reverse" [1].

We have a similar problem with applicative functors:

( (fun a b -> (b, b, a))
  <$> (pa : a t)
  <*> (pb : b t) ) : (b * b * a) t

(Given the usual <$> : ('a -> 'b) -> 'a t -> 'b t and <*> : ('a -> 'b) t -> 'a t -> 'b t.) Although the elements of ASN syntax are now exposed, the process of going from intermediate parsing results to the result of the whole is still not accessible.

Fortunately, due to the regular structure of ASN, we don't really need the full expressive power of monadic parsing. The only occurrence of sequential parsing is within SEQUENCE and related constructs, and we don't need look-ahead. All we need to do is provide a few specialized combinators to handle those cases -- combinators the likes of which would be derived in a more typical setting.

So if we imagine we had a few values, like:

val gen_time : gen_time t
val utc_time : utc_time t
val choice   : 'a t -> 'b t -> ('a, 'b) choice t
val sequence : 'a t -> 'b t -> ('a * 'b) t

Assuming appropriate OCaml types gen_time and utc_time that reflect their ASN counterparts, and a simple sum type choice, we could express the Validity grammar above using:

type time = (gen_time, utc_time) choice
let time     : time t          = choice gen_time utc_time
let validity : (time * time) t = sequence time time

In fact, ASN maps quite well to algebraic data types. Its SEQUENCE corresponds to n-ary products and CHOICE to sums. ASN SET is a lot like SEQUENCE, except the elements can come in any order; and SEQUENCE_OF and SET_OF are just lifting an 'a-grammar into an 'a list-grammar.

A small wrinkle is that SEQUENCE allows for more contextual information on its components (so does CHOICE in reality, but we ignore that): elements can carry labels (which are not used for parsing) and can be marked as optional. So instead of working directly on the grammars, our sequence must work on their annotated versions. A second wrinkle is the arity of the sequence combinator.

Thus we introduce the type of annotated grammars, 'a element, which corresponds to one ,-delimited syntactic element in ASN's own SEQUENCE grammar, and the type 'a sequence, which describes the entire contents ({ ... }) of a SEQUENCE definition:

val required : 'a t -> 'a element
val optional : 'a t -> 'a option element
val ( -@ )   : 'a element -> 'b element -> ('a * 'b) sequence
val ( @ )    : 'a element -> 'a sequence -> ('a * 'b) sequence
val sequence : 'a sequence -> 'a t

The following are then equivalent:

Triple ::= SEQUENCE {
  a INTEGER,
  b BOOLEAN,
  c BOOLEAN OPTIONAL
}

let triple : (int * (bool * bool option)) t =
  sequence (
      required int
    @ required bool
   -@ optional bool
  )

We can also re-introduce functions, but in a controlled manner:

val map : ('a -> 'b) -> ('b -> 'a) -> 'a t -> 'b t

Keeping in line with the general theme of bidirectionality, we require functions to come in pairs. The deceptively called map could also be called iso, and comes with a nice property: if the two functions are truly inverses, the serialization process is fully reversible, and so is parsing, under single-representation encodings (DER)!

ASTs of ASNs

To go that last mile, we should probably also implement what we discussed.

Traditional parser combinators look a little like this:

type 'a p = string -> 'a * string

let bool : bool p = fun str -> (s.[0] <> "\\000", tail_of_string str)

Usually, the values inhabiting the parser type are the actual parsing functions, and their composition directly produces larger parsing functions. We would probably need to represent them with 'a p * 'a s, pairs of a parser and its inverse, but the same general idea applies.

Nevertheless, we don't want to do this. The grammars need to support more than one concrete parser/serializer, and composing what is common between them and extracting out what is not would probably turn into a tangled mess. That is one reason. The other is that if we encode the grammar purely as (non-function) value, we can traverse it for various other purposes.

So we turn from what is sometimes called "shallow embedding" to "deep embedding" and try to represent the grammar purely as an algebraic data type.

Let's try to encode the parser for bools, boolean : bool t:

type 'a t =
  | Bool
  ...

let boolean : bool t = Bool

Unfortunately our constructor is fully polymorphic, of type 'a. 'a t. We can constrain it for the users, but once we traverse it there is nothing left to prove its intended association with booleans!

Fortunately, starting with the release of OCaml 4.00.0, OCaml joined the ranks of languages equipped with what is probably the supreme tool of deep embedding, GADTs. Using them, we can do things like:

type _ t =
  | Bool   : bool t
  | Pair   : ('a t * 'b t) -> ('a * 'b) t
  | Choice : ('a t * 'b t) -> ('a, 'b) choice t
  ...

In fact, this is very close to how the library is actually implemented.

There is only one thing left to worry about: ASN definitions can be recursive. We might try something like:

let rec list = choice null (pair int list)

But this won't work. Being just trees of applications, our definitions never contain statically constructive parts -- this expression could never terminate in a strict language.

We can get around that by wrapping grammars in Lazy.t (or just closures), but this would be too awkward to use. Like many other similar libraries, we need to provide a fixpoint combinator:

val fix : ('a t -> 'a t) -> 'a t

And get to write:

let list = fix @@ fun list -> choice null (pair int list)

This introduces a small problem. So far we simply reused binding inherited from OCaml without ever worrying about identifiers and references, but with a fixpoint, the grammar encodings need to be able to somehow express a cycle.

Borrowing an idea from higher-order abstract syntax, we can represent the entire fixpoint node using exactly the function provided to define it, re-using OCaml's own binding and identifier resolution:

type _ t =
  | Fix : ('a t -> 'a t) -> 'a t
  ...

This treatment completely sidesteps the problems with variables. We need no binding environments or De Brujin indices, and need not care about the desired scoping semantics. A little trade-off is that with this simple encoding it becomes more difficult to track cycles (when traversing the AST, if we keep applying a Fix node to itself while descending into it, it looks like an infinite tree), but with a little opportunistic caching it all plays out well [2].

The parser and serializer proper then emerge as interpreters for this little language of typed trees, traversing them with an input string, and parsing it in a fully type-safe manner.

How does it play out?

The entire ASN library comes down to ~1,700 lines of OCaml, with around ~1,100 more in tests, giving a mostly-complete treatment of BER and DER.

Its main use so far is in the context of the X.509 library (discussed yesterday). It allowed the grammar of certificates and RSA keys, together with a number of transformations from the raw types to more pleasant, externally facing ones, to be written in ~900 lines of OCaml. And the code looks a lot like the actual standards the grammars were taken from -- the fragment from the beginning of this article becomes:

let unique_identifier = bit_string_cs

let time =
  map (function `C1 t -> t | `C2 t -> t) (fun t -> `C2 t)
      (choice2 utc_time generalized_time)

let validity =
  sequence2
    (required ~label:"not before" time)
    (required ~label:"not after"  time)

We added ~label to 'a element-forming injections, and have:

val choice2 : 'a t -> 'b t -> [ `C1 of 'a | `C2 of 'b ] t

To get a sense of how the resulting system eases the translation of standardized ASN grammars into working code, it is particularly instructive to compare these two definitions.

Reversibility was a major simplifying factor during development. Since the grammars are traversable, it is easy to generate their random inhabitants, encode them, parse the result and verify the reversibility still holds. This can't help convince us the parsing/serializing pair is actually correct with respect to ASN, but it gives a simple tool to generate large amounts of test cases and convince us that that pair is equivalent. A number of hand-written cases then check the conformance to the actual ASN.

As for security, there were two concerns we were aware of. There is a history of catastrophic buffer overruns in some ASN.1 implementations, but -- assuming our compiler and runtime system are correct -- we are immune to these as we are subject to bounds-checking. And there are some documented problems with security of X.509 certificate verification due to overflows of numbers in ASN OID types, which we explicitly guard against.

You can check our security status on our issue tracker.

Footnotes

1. In fact, the problem with embedding functions in combinator languages, and the fact that in a functional language it is not possible to extract information from a function other than by applying it, was discussed more than a decade ago. Such discussions led to the development of Arrows, amongst other things.

2. Actually, a version of the library used the more proper encoding to be able to inject results of reducing referred-to parts of the AST into the referring sites directly, roughly like Fix : ('r -> ('a, 'r) t) -> ('a, 'r) t. This approach was abandoned because terms need to be polymorphic in 'r, and this becomes impossible to hide from the user of the library, creating unwelcome noise.

---

Posts in this TLS series:

• Introducing transport layer security (TLS) in pure OCaml
• OCaml-TLS: building the nocrypto library core
• OCaml-TLS: adventures in X.509 certificate parsing and validation
• OCaml-TLS: ASN.1 and notation embedding
• OCaml-TLS: the protocol implementation and mitigations to known attacks