Title: Narcissus: Deriving Correct-By-Construction Decoders and Encoders from Binary Formats,
Abstract: It is a neat result from functional programming that libraries of parser
combinators can support rapid construction of decoders for quite a range of
formats. With a little more work, the same combinator program can denote both a
decoder and an encoder. Unfortunately, the real world is full of gnarly
formats, as with the packet formats that make up the standard Internet protocol
stack. Most past parser-combinator approaches cannot handle these formats, and
the few exceptions require redundancy -- one part of the natural grammar needs
to be hand-translated into hints in multiple parts of a parser program. We show
how to recover very natural and nonredundant format specifications, covering
all popular network packet formats and generating both decoders and encoders
automatically. The catch is that we use the Coq proof assistant to derive both
kinds of artifacts using tactics, automatically, in a way that guarantees that
they form inverses of each other. We used our approach to reimplement packet
processing for a full Internet protocol stack, inserting our replacement into
the OCaml-based MirageOS unikernel, resulting in minimal performance
degradation.