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
- Authors' version (also at the Cryptology ePrint archive)
- GitHub repository of the packet protection layer
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.