A Security Model and Fully Verified Implementation for the IETF QUIC Record Layer

Antoine Delignat-Lavaud (Programming Principles and Tools, Microsoft Research, Cambridge, United Kingdom)
Cédric Fournet (Programming Principles and Tools)
Bryan Parno (Computer Science Department, Carnegie Mellon University, Pittsburgh, PA, USA; Electrical and Computer Engineering Department, Carnegie Mellon University)
Jonathan Protzenko (RiSE: Research in Software Engineering, Microsoft Research, Redmond, WA, USA)
Tahina Ramananandro (RiSE)
Jay Bosamiya (CMU ECE)
Joseph Lallemand (INRIA Nancy Grand-Est, LORIA)
Itsaka Rakotonirina (INRIA Nancy Grand-Est, LORIA)
Yi Zhou (CMU ECE)

IEEE S&P 2021 (42nd IEEE Symposium on Security and Privacy, a.k.a. "Oakland")
Accepted for publication, to appear

Drawing on earlier protocol-verification work, we investigate the security of the QUIC record layer, as standardized by the IETF in draft version 24. This version features major differences compared to Google's original protocol and prior IETF drafts. It serves as a useful test case for our verification methodology and toolchain, while also, hopefully, drawing attention to a little studied yet crucially important emerging standard.
We model QUIC packet and header encryption, which uses a custom construction for privacy. To capture its goals, we propose a security definition for authenticated encryption with semi-implicit nonces. We show that QUIC uses an instance of a generic construction parameterized by a standard AEAD-secure scheme and a PRF-secure cipher. We formalize and verify the security of this construction in F*. The proof uncovers interesting limitations of nonce confidentiality, due to the malleability of short headers and the ability to choose the number of least significant bits included in the packet counter. We propose improvements that simplify the proof and increase robustness against strong attacker models. In addition to the verified security model, we also give a concrete functional specification for the record layer, and prove that it satisfies important functionality properties (such as successful decryption of encrypted packets) after fixing more errors in the draft. We then provide a high-performance implementation of the record layer that we prove to be memory safe, correct with respect to our concrete specification (inheriting its functional correctness properties), and secure with respect to our verified model. To evaluate this component, we develop a provably-safe implementation of the rest of the QUIC protocol. Our record layer achieves nearly 2 GB/s throughput, and our QUIC implementation's performance is within 21% of an unverified baseline.