NARCISSUS: Deriving Correct-By-Construction Decoders and Encoders from Binary Formats

Research Areas: End System Security

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.

Personnel

Students: Qianchuan Ye

Representative Publications

Benjamin Delaware, Sorawit Suriyakarn, Clément Pit-Claudel, Qianchuan Ye, and Adam Chlipala. 2019. Narcissus: correct-by-construction derivation of decoders and encoders from binary formats. Proc. ACM Program. Lang. 3, ICFP, Article 82 (August 2019), 29 pages. https://doi.org/10.1145/3341686
```
 
```
- Qianchuan Ye and Benjamin Delaware. 2019. A verified protocol buffer compiler. In Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2019). Association for Computing Machinery, New York, NY, USA, 222–233. https://doi.org/10.1145/3293880.3294105
```
 
```

Keywords: Binary Formats, High Assurance Software, Theorem Proving