A Formal Semantics for ASN.1
Presented as part of the 2007 HCSS conference.
Abstract
Abstract Syntax Notation number One (ASN.1) is an international standard domain specific language (DSL) for describing data formats in a platform-independent manner, allowing communication among applications running on different platforms. It is used to describe the message formats for numerous Internet and security protocols, such as X.400, X.500, SNMP, and X.509, and in particular the secure sockets library SSL/TLS. There is a known instance of a security vulnerability in an SSL implementation due to incorrect ASN.1 encode/decode code.
There are many ASN.1 compilers. Most are proprietary solutions that make examination of the source code to achieve higher confidence impossible. Even when source code is available, the majority of ASN.1 compilers are written in general purpose imperative languages that make assurance more difficult.
Galois is building the High Assurance ASN.1 Workbench (HAAW), consisting of an ASN.1 compiler, interpreter, test case generator, and support for formal verification of the correctness and safety of the generated code. We developed a proof-of-concept compiler in 2004, and we now have a beta of an ASN.1 interpreter.
As part of our work on the ASN.1 interpreter, we’ve written a denotational semantics for a rich subset of ASN.1. In a denotational semantics for a programming language, program phrases map to well-understood mathematical objects. For ASN.1, our semantics maps data specifications to Haskell code that expresses the meaning of those specifications. In particular, it maps type definitions to Haskell encoders and decoders for those types. Our encoders and decoders work on abstract data streams that capture the information that’s used in actual encodings to octets, while preserving readability and glossing over some low-level details. We’ve written a translation layer that can translate between abstract data streams and DER.
Because the denotations are executable, we can test our semantics directly on ASN.1 specifications. We’ve run it on a corpus of automatically-generated tests, as well as a number of hand-written tests. Some of the tests check whether the encoders and decoders are inverses. Others check that well-formed specifications have a meaning in the semantics. Still other tests check the semantics encoding against that produced by the interpreter, using the DER translation layer, to assess the correctness of the interpreter.