EverParse: Verified Secure Zero-Copy Parsers for Authenticated Message Formats
2019
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.
- Correction
- Source
- Cite
- Save
- Machine Reading By IdeaReader
0
References
0
Citations
NaN
KQI