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

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.