NDSS

February, 23, 2020
NDSS 2020

Abstract. Inspired by the TLS Ready or Not (TRON) workshop at NDSS in 2016, QUIPS was a workshop focusing on QUIC security and privacy analysis efforts. Its goal was to bring formal analysis results to the IETF working group and developer communities in order to build confidence in and improve QUIC before its widespread deployment.

Overview

The IETF QUIC protocol is a modern UDP-based, stream-multiplexing, encrypted transport protocol. Inspired by prior art, QUIC’s packet and header encryption removes cleartext  information from the network while simultaneously mitigating ossification of version-specific protocol behavior. As one example, QUIC’s standard packet header is almost fully encrypted and authenticated. To aid network operator debugging, a single (optional) bit in the header is reserved for use as a means of coarsely measuring end-to-end RTT.

The delta between TLS 1.3 (over TCP) and QUIC as secure transport protocols is non-negligible. In particular, there are several facets of the design that warrant further analysis, including, though not limited to the following:

  1. Cryptographic handshake integration. Designed with TLS 1.3 [RFC8446] as the authenticated key exchange protocol (AKE), QUIC uses state-of-the-art cryptography for establishing and using shared session secrets for packet encryption. Consequently, QUIC also benefits from extensive security analysis efforts that helped standardize TLS 1.3. However, QUIC’s modular design and the integration of TLS 1.3 in particular, has not yet received formal analysis.
  2. Packet protection. Analysis of TLS assumed ordered delivery, whereas QUIC does not enjoy that benefit. The effect of packet loss on QUIC’s record layer security is important and not well understood. Moreover, QUIC’s record layer provides features that TLS does not, such as header protection. Capturing the semantics of this new packet protection algorithm and proving them correct is critical.
  3. Denial of Service (DoS) features. QUIC has a number of features designed to reduce the effects of DoS, both on individual connections, such as duplicate packet detection and complete packet protection, server resources, such as Retry, and the resources of bystanders, such as anti-reflection. It has yet to be shown whether or not these techniques achieve their desired goals.
  4. Privacy. Many of QUIC’s features account for and attempt mitigation of packet linkability across network paths and between different connections. For example, voluntary connection migration requires endpoints to use new connection identifiers if possible as a way of preventing cross-path linkability. Also, as a means of improving endpoint privacy postures, among others, QUIC does not mandate endpoints provide any way for networks to measure per-connection Round Trip Time (RTT). The optional spin bit is the only signal made willingly available to the network. Currently, there is no strong analysis supporting the concrete privacy benefits these features provide to QUIC endpoints.

Other remaining issues include stateless reset, accepting signals from the network for PMTUD and ECN, among others.

In its current state, the QUIC draft specifications have yet to receive comprehensive security or privacy analysis. Similar to TLS 1.3, there is a limited amount of time for this analysis before the protocol is standardized. And this analysis is a critical step towards ensuring safety, correctness, security, and privacy aspects of this emerging protocol.

QUIC Security and Privacy (QUIPS) was a workshop held at NDSS 2020 with the goal of creating a medium through which QUIC security and privacy analysis efforts can be brought to the attention of the IETF and developer communities, in order to build confidence in and improve QUIC before its widespread deployment. QUIPS solicited papers and talks on all aspects of the security of the QUIC protocol or implementations thereof. The goal was to present and discuss those submissions at the workshop in the presence of the designers and early implementers of QUIC and other attendees, so that the soundness of QUIC can be ascertained and any weaknesses that are identified can be mitigated or documented in a timely fashion.

QUIPS consisted of two main sessions, followed by a Q&A panel comprised of session attendees. The morning session featured peer-reviewed papers submitted to the workshop. The afternoon session featured invited talks and previously published works relevant to QUIPS topics. 

This document summarizes the workshop presentations and panel session. In doing so, it highlights problems identified for the continued development of QUIC.

Papers and Talks

Peer-Reviewed Research Papers

A Security Model and Verified Implementation for the IETF QUIC Transport Protocol

Antoine Delignat-Lavaud, Cédric Fournet, Bryan Parno, Jonathan Protzenko, Tahina Ramananandro, Jay Bosamiya, Joseph Lallemand, Itsaka Rakotonirina, Yi Zhou

Abstract: We investigate the security of the QUIC transport, as standardized by the IETF in draft version 24. This version features major differences compared to Google’s original protocol and prior IETF drafts. We model packet and header encryption, which uses a custom construction for privacy. We propose a new 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 implement the concrete functional specification, and prove that it satisfies important correctness properties (such as successful decryption of encrypted packets) after fixing more errors in the draft. Lastly, we provide a high-performance Low* implementation of packet stream encryption built on top of the verified EverCrypt crypto provider and the EverParse message formatting library, 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 write a partial implementation of the QUIC transport in Dafny, and prove its memory safety once extracted to C++.

Two-Tier Authenticated Encryption: Nonce Hiding in QUIC

Mihir Bellare, Felix Günther, and Bjoern Tackmann


Abstract: The QUIC protocol introduces QUIC Packet Encryption (QPE) to protect the data during transmission. QPE encrypts the payload with nonce-based authenticated encryption. Part of the nonce, for which QUIC uses a sequence number, is transmitted with the ciphertext but is additionally, together with parts of the header, masked in order to prevent traffic analysis.

Motivated by QUIC’s use of one key for the masking and another key for the payload encryption, we begin by modeling two-tier encryption schemes that encrypt and decrypt different parts of the ciphertext using different keys, and possibly with different security properties. We explicitly model the guarantees required by the scheme used in QUIC, namely that the payload encryption is authenticated, while the masking scheme only ensures that a modification of the ciphertext will predictably induce a corresponding modification of the plaintext. The goal of this modeling is to formalize statements about the expected properties of QUIC, such as nonce-hiding and the ability to achieve forward secrecy by rotating the payload encryption key.

As a first step, we use the recent framework for nonce-hiding authenticated encryption of Bellare, Ng, and Tackmann (CRYPTO 2019) to analyze the encryption of the nonce. We model QPE as a type of nonce-based encryption scheme where encryption takes a pair (N_i, N_e) of nonces, but decryption obtains only N_e. This syntax, which was already present in the CAESAR call and was called AE5 by Namprempre, Rogaway, and Shrimpton, generalizes both the standard nonce-based encryption syntax (NBE1), where decryption obtains the full nonce, and the NBE2 syntax of Bellare et al., where the decryption does not obtain the nonce. We adapt the definitions of Bellare et al., and model and prove that QPE is partially nonce-hiding in the sense that it hides N_e.

Secure Communication Channel Establishment: TLS 1.3 (over TCP Fast Open) vs. QUIC

Shan Chen, Samuel Jero, Matthew Jagielski, Alexandra Boldyreva and Cristina Nita-Rotaru

Slides: TBD

Abstract: Secure channel establishment protocols such as Transport Layer Security (TLS) are some of the most important cryptographic protocols, enabling the encryption of Internet traffic. Reducing the latency (the number of interactions between parties) in such protocols has become an important design goal to improve user experience. The most important protocols addressing this goal are the just-released TLS 1.3, which is likely to see deployment in the near future, and Quick UDP Internet Connections (QUIC), a secure transport protocol from Google that is available in the Chrome browser. There have been a number of formal security analyses for TLS 1.3 and QUIC, but their security, when layered with their underlying transport protocols, cannot be easily compared. Our work is the first to thoroughly compare the security and availability properties of these protocols. Towards this goal, we develop novel security models that permit “layered” security analysis. In addition to the standard goals of server authentication and data privacy and integrity, we consider the goals of IP spoofing prevention, key exchange packet integrity, secure channel header integrity, and reset authentication, which capture a range of practical threats not usually taken into account by existing security models that focus mainly on the cryptographic cores of the protocols. Equipped with our new models we provide a detailed comparison of TLS 1.3 over TCP Fast Open (TFO), QUIC over UDP, and QUIC[TLS] (a new design for QUIC that uses TLS 1.3 key exchange) over UDP. In particular, we show that TFO’s cookie mechanism does provably achieve the security goal of IP spoofing prevention. Additionally, we find several new availability attacks that manipulate the early key exchange packets without being detected by the communicating parties. By including packet-level attacks in our analysis, our results shed light on how the reliability, flow control, and congestion control of the above layered protocols compare, in adversarial settings. We hope that our results will help protocol designers in their future protocol analyses and that our results will help practitioners better understand the advantages and limitations of novel secure channel establishment protocols.

QuicR: QUIC Resiliency to BW-DoS Attacks

Ori Hiba, Amir Herzberg, and Hemi Leibowitz

Slides: TBD

Abstract: We present QuicR, an adaptation of the QUIC protocol, which is resilient to congestion(BW-DoS attacks). Specifically, QuicR uses Forward Error Correction (FEC) to ensure reliable communication between applications, even when using lossy, high-latency connections, as is common under clogging. QuicR can be easily deployed by applications, using TCP-like API,and supports different application requirements, includingFIFO / non-FIFO, lossy / non-lossy,elastic / inelastic (QoS)traffic and optional caching of responses to queries.We describe the design and an initial, partial implementation of QuicR. We also present experimental evaluation of this implementation, confirming that it performs well under a different realistic scenarios. We focus on high loss-rate and latency scenarios, typical to BW-DoS attacks, where both TCP and QUIC fail or perform poorly.

Robust Channels: Handling Unreliable Network Messages in QUIC’s Record Layer

Marc Fischlin, Felix Günther, and Christian Janson


Abstract: The common approach in channel protocols is to rely on ciphertexts arriving in-order and close the connection upon any rogue ciphertext, and cryptographic security models for channels generally reflect such design. This is reasonable when running atop lower-level transport protocols like TCP ensuring in-order delivery, as for example is the case with TLS or SSH. However, channels such as QUIC or DTLS which run over a non-reliable transport protocol like UDP, do not—and in fact cannot—close the connection if packages are lost or arrive in a different order. Those protocols instead have to carefully catch such effects arising naturally in unreliable networks by using a sliding-window technique where ciphertexts can be decrypted correctly as long as they are not misplaced too far. To accommodate such handling of unreliable network messages, we introduce a generalized notion of robustness to cryptographic channel modeling. This property can capture unreliable network behavior and guarantees that adversarial tampering cannot hinder ciphertexts that can be decrypted correctly from being accepted. As one particularly interesting target, we capture the packet encryption in QUIC’s record layer as a cryptographic channel protocol and show that it achieves the intended level of robustness based on certain properties of the sliding-window technique and the underlying AEAD scheme.

Invited Talks

QUIC Security Summary

Martin Thomson


Summary: A summary of QUIC’s design and security features will be presented. Open issues and areas requiring further analysis will be identified and discussed.

On Wire Images

Brian Trammell


Summary: TBD

Authenticated QUIC Handshakes

Chris Wood (on behalf of Christian Huitema and Kazuho Oku)


Summary: This talk will explain a proposal that uses a variant of QUIC protocol version 1 that uses TLS Encrypted Client Hello (ECHO) keys to authenticate the Initial packets thereby making the entire handshake tamper-proof.

nQUIC (Noise + QUIC)

Mathias Hall-Andersen, David Wong, Nick Sullivan, and Alishah Chator


Summary: We present nQUIC, a variant of QUIC-TLS that uses the Noise protocol framework for its key exchange and basis of its packet protector with no semantic transport changes. nQUIC is designed for deployment in systems and for applications that assert trust in raw public keys rather than PKI-based certificate chains. It uses a fixed key exchange algorithm, compromising agility for implementation and verification ease. nQUIC provides mandatory server and optional client authentication, resistance to Key Compromise Impersonation attacks, and forward and future secrecy of traffic key derivation, which makes it favorable to QUIC-TLS for long-lived QUIC connections in comparable applications. We developed two interoperable prototype implementations written in Go and Rust. Experimental results show that nQUIC finishes its handshake in a comparable amount of time as QUIC-TLS.

Towards Securing the Internet of Things with QUIC

Lars Eggert


Summary: This paper is the first to evaluate the feasibility of deploying QUIC, a new UDP-based transport protocol currently undergoing IETF standardization, directly on resource-constrained IoT devices. It quantifies the storage, compute, memory and energy requirements of the Quant QUIC stack on two different IoT platforms, and finds that a minimal standards-compliant QUIC client currently requires approximately 58 to 63 KB of flash and can retrieve 5 KB of data in 4.2 to 5.1 s over 0-RTT or 1-RTT connections, using less than 16 KB of heap memory (plus packet buffers), less than 4 KB of stack memory and less than 0.9 J of energy per transaction.

Panel Q&A

The panel session discussed a variety of topics. (Detailed minutes of the session are in Appendix A.) Summaries of comments and observations made during the session are below.

  • Lack of confidence in protocol correctness coupled with a lack of version negotiation is potentially crippling. One of these should ideally be fixed before the RFC mints. 
  • We don’t fully understand the TLS abstraction that QUIC utilizes. (It’s underspecified.) Perhaps work should be done to try and better document this interface, at least as is done by the few TLS stacks in use by QUIC implementations? This may help future changes should we need to adjust the interface or the underlying AKE protocol.
  • 0-RTT was easy to implement in comparison to that in TLS 1.3, which was significantly more challenging. Moreover, implementations changed so much over time that it might be best for folks to start from scratch rather than continue re-iterating on existing code bases.
  • Traffic analysis is, as always, a challenging topic. How much do we do to deter it? (Constant-time packet processing? Spatial or temporal padding? Or both?)
  • QUIC forced a new transport interface onto developers beyond traditional sockets. This was ultimately better in the long run, but this made things difficult.

Discussion and Future Work

The workshop raised interesting points with respect to QUIC’s current security and privacy posture. Critical questions that need further study are below. 

  • What should be the re-key frequency? The robust channels paper suggests it should take into account unreliable transport properties (i.e., a security degradation linear not alone in the number of successfully sent/received packets, but also in the number of rejected packets). The analysis done for TLS claims to consider DTLS, which would translate to QUIC, but there is some concern that it doesn’t. More work is needed.
  • Can we use formal analysis tools to assert protocol correctness, i.e., to show that further deadlocks are not possible? And if not, can we bring back Version Negotiation as a mandatory feature or extension for V1? (Otherwise, how do we deal with fundamental protocol flaws that we can’t patch with a new version? Is reliance on Alt-Svc discovery fine for now?)

Several non-critical comments, open questions, and areas of further work were also raised. These are summarized below:

  • Can we invest more in implementation test software, such as that from Jana and Marten?
  • We should better understand the impact of unauthenticated signals (ECN markings, ICMP packets, failed decryption, etc) on internal protocol state.
  • How do we deal with unauthenticated CID lengths and packet format malleability? (That is, how can we prevent the draft -13 packet number encryption bug?)
  • Should we authenticate the DCID?
  • Is there no way to rotate the header protection key? For example, could we derive candidates for each epoch and do trial decryption? Or generalize “2-tier” header protection (of the two-tier AE paper) to do 3-tier encryption?
  • No clear delineation between 0-RTT and 1-RTT application data. Should there be? How do (or should) APIs reflect this?
  • What more can we gain by encrypting more information (such as the CID)? At what point can we declare victory against (active) attackers? (What sort of confidentiality goals are we comfortable stating about QUIC? Would they be similar to that of TLS?)
  • What is the TLS and QUIC feature overlap? What can and should be moved from TLS to QUIC? Did we find the right abstraction?
  • Should we have introduced a “handshake secret” exporter interface for TLS rather than use handshake secrets directly?

Some “nice to have” comments were also raised during the workshop. These are summarized below.

  • Can we add some text which shows or asserts that QUIC’s packet protection achieves the same guarantees (as required by proofs) of the TLS record layer?
  • Can we document malleability properties of QUIC packets, or the lack thereof?
  • Can we document the abstract interface of TLS as an AKE in QUIC? There are many QUIC implementations, yet few dependent TLS implementations, and this interface is not well documented outside of code.
  • Should we expand constant-time considerations? Is constant-time packet de-protection required? What about frame processing? At what point do we stop trying to mitigate against side channels? And how should we deal with traffic analysis in general?
  • There are some requirements in the spec that we have seen violated by implementations, such a non-CT packet protection removal, use of 1-RTT prior to handshake completion. Do we build a new TLS to address those? Is that justified?