NARCISSUS: Deriving Correct-By-Construction Decoders and Encoders from Binary Formats
Principal Investigator: Benjamin Delaware
NARCISSUS is a framework for automatically synthesizing high-assurance serializer and deserializers from high-level specifications. The starting point of the process is a binary format, expressed as a relation which precisely captures all the valid binary encodings of an arbitrary datatype instance. From this specification, NARCISSUS synthesizes a decoder that is guaranteed to be the inverse of this relation, drawing on an extensible set of decoding strategies to construct the implementation. Each decoder is furthermore guaranteed to detect malformed encodings by failing on inputs not included in this relation. The derivation is carried out inside the Coq proof assistant and produces a proof trail certifying the correctness of the synthesized decoder. We have demonstrated the utility of our framework by deriving and evaluating the performance of decoders for all packet formats used in a standard network stack.