Narcissus: correct-by-construction derivation of decoders and encoders from binary formats

• Main Authors: Pit-Claudel, Clement Francois (Author), Chlipala, Adam (Author)
• Other Authors: Massachusetts Institute of Technology. Department of Electrical Engineering and Computer Science (Contributor)
• Format: Article
• Language: English
• Published: Association for Computing Machinery (ACM), 2021-02-26T16:02:49Z.
• Subjects: Article
• Online Access: Get fulltext

 It is a neat result from functional programming that libraries ofparser combinatorscan support rapid construc-tion of decoders for quite a range of formats. With a little more work, the same combinator program can denoteboth a decoder and an encoder. Unfortunately, the real world is full of gnarly formats, as with the packetformats that make up the standard Internet protocol stack. Most past parser-combinator approaches cannothandle these formats, and the few exceptions require redundancy - one part of the natural grammar needs tobe hand-translated into hints in multiple parts of a parser program. We show how to recover very naturaland nonredundant format specifications, covering all popular network packet formats and generating bothdecoders and encoders automatically. The catch is that we use the Coq proof assistant to derive both kinds ofartifacts using tactics, automatically, in a way that guarantees that they form inverses of each other. We usedour approach to reimplement packet processing for a full Internet protocol stack, inserting our replacementinto the OCaml-based MirageOS unikernel, resulting in minimal performance degradation.