Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Verifying QUIC implementations using Ivy

Christophe Crochet, Tom Rousseaux, J-F Sambon, Maxime Piraux, Axel Legay

TL;DR

This work extends the Ivy framework to QUIC by updating the formal model to IETF draft-29, expanding Connection ID support, and implementing transport-error tests. It automates comprehensive testing across seven QUIC servers and seven clients, revealing broad variability in implementation maturity and exposing ambiguities in the QUIC specification. The approach uses network-centric compositional testing to generate diverse test traces from the Ivy model and uncovers areas where the spec lacks precision, particularly around migration behavior and error handling. The findings demonstrate the value of formal, automated verification for protocol conformance and provide concrete directions to improve QUIC specifications and implementations.

Abstract

QUIC is a new transport protocol combining the reliability and congestion control features of TCP with the security features of TLS. One of the main challenges with QUIC is to guarantee that any of its implementation follows the IETF specification. This challenge is particularly appealing as the specification is written in textual language, and hence may contain ambiguities. In a recent work, McMillan and Zuck proposed a formal representation of part of draft-18 of the IETF specification. They also showed that this representation made it possible to efficiently generate tests to stress four implementations of QUIC. Our first contribution is to complete and extend the formal representation from draft-18 to draft-29. Our second contribution is to test seven implementations of both QUIC client and server. Our last contribution is to show that our tool can highlight ambiguities in the QUIC specification, for which we suggest paths to corrections

Verifying QUIC implementations using Ivy

TL;DR

This work extends the Ivy framework to QUIC by updating the formal model to IETF draft-29, expanding Connection ID support, and implementing transport-error tests. It automates comprehensive testing across seven QUIC servers and seven clients, revealing broad variability in implementation maturity and exposing ambiguities in the QUIC specification. The approach uses network-centric compositional testing to generate diverse test traces from the Ivy model and uncovers areas where the spec lacks precision, particularly around migration behavior and error handling. The findings demonstrate the value of formal, automated verification for protocol conformance and provide concrete directions to improve QUIC specifications and implementations.

Abstract

QUIC is a new transport protocol combining the reliability and congestion control features of TCP with the security features of TLS. One of the main challenges with QUIC is to guarantee that any of its implementation follows the IETF specification. This challenge is particularly appealing as the specification is written in textual language, and hence may contain ambiguities. In a recent work, McMillan and Zuck proposed a formal representation of part of draft-18 of the IETF specification. They also showed that this representation made it possible to efficiently generate tests to stress four implementations of QUIC. Our first contribution is to complete and extend the formal representation from draft-18 to draft-29. Our second contribution is to test seven implementations of both QUIC client and server. Our last contribution is to show that our tool can highlight ambiguities in the QUIC specification, for which we suggest paths to corrections

Paper Structure

This paper contains 11 sections, 2 figures, 6 tables.

Table of Contents

  1. Introduction
  2. The brief overview of Ivy model for QUIC IETF Draft-29
  3. On Generating Test Cases
  4. Example
  5. On testing server implementations
  6. On testing client implementations
  7. Results
  8. Migration issues
  9. Migration issues: Case study I
  10. Migration issues: Case study II
  11. Transport error code issues

Figures (2)

  • Figure 1: Tool coverage of requirements in the QUIC specification
  • Figure 2: The QUIC frame component (resp. QUIC packet component) randomly generates frames (resp. packets) meeting its requirements, selects some of them and transmit them to the next node. The shim is the last node: it is the interface between the abstract representation of the model and the network. Valid QUIC transmissions are generated from left to right while received transmission are verified from right to left.