EverParse: Verified Secure Zero-Copy Parsers for Authenticated Message Formats

Tahina Ramananandro (RiSE: Research in Software Engineering, Microsoft Research, Redmond, WA, USA)
Antoine Delignat-Lavaud (Programming Principles and Tools, Microsoft Research, Cambridge, United Kingdom)
Cédric Fournet (Programming Principles and Tools)
Nikhil Swamy (RiSE)
Tej Chajed (Parallel & Distributed Operating Systems, CSAIL, MIT)
Nadim Kobeissi (NYU Paris; Symbolic Software)
Jonathan Protzenko (RiSE)

USENIX Security 2019

• Final version on the USENIX Security website
• Presentation by Antoine Delignat-Lavaud at USENIX Security:
  • YouTube Video
  • PowerPoint Slides
  • PDF Slides
• Paper preprint
• GitHub repository

We present EverParse, a framework for generating parsers and serializers from tag-length-value binary message format descriptions. The resulting code is verified to be safe (no overflow, no use after free), correct (parsing is the inverse of serialization) and non-malleable (each message has a unique binary representation). These guarantees underpin the security of cryptographic message authentication, and they enable testing to focus on interoperability and performance issues.

EverParse consists of two parts: LowParse, a library of parser combinators and their formal properties written in F*; and QuackyDucky, a compiler from a domain-specific language of RFC message formats down to low-level F* code that calls LowParse. While LowParse is fully verified, we do not formalize the semantics of the input language and keep QuackyDucky outside our trusted computing base. Instead, it also outputs a formal message specification, and F* automatically verifies our implementation against this specification.

EverParse yields efficient zero-copy implementations, usable both in F* and in C. We evaluate it in practice by fully implementing the message formats of the Transport Layer Security standard and its extensions (TLS 1.0--1.3, 293 datatypes) and by integrating them into miTLS, an F* implementation of TLS. We illustrate its generality by implementing the Bitcoin block and transaction formats, and the ASN.1 DER payload of PKCS#1 RSA signatures. We integrate them into C applications and measure their runtime performance, showing significant improvements over prior handwritten libraries.