Verifying QUIC Implementations using Ivy
Fri, 10/29/2021 - 12:37 by Maxime Piraux
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.
- Authors
- Christophe Crochet, Tom Rousseaux, Maxime Piraux, Jean-François Sambon and Axel Legay
- Source
Workshop on the Evolution, Performance and Interoperability of QUIC (EPIQ’21) , 2021.
- Full text
-
(564.36 KB) - Cite it
- BibTex
- Copyright
- See here
IEEE Copyright Notice: This material is presented to ensure timely dissemination of scholarly and technical work. Copyright and all rights therein are retained by authors or by other copyright holders. All persons copying this information are expected to adhere to the terms and constraints invoked by each author's copyright. In most cases, these works may not be reposted without the explicit permission of the copyright holder.
ACM Copyright Notice: Copyright 1999 by the Association for Computing Machinery, Inc. Permission to make digital or hard copies of part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page or intial screen of the document. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, to republish, to post on servers, or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from Publications Dept., ACM Inc., fax +1 (212) 869-0481, or permissions@acm.org.
Springer-Verlag LNCS Copyright Notice: The copyright of these contributions has been transferred to Springer-Verlag Berlin Heidelberg New York. The copyright transfer covers the exclusive right to reproduce and distribute the contribution, including reprints, translations, photographic reproductions, microform, electronic form (offline, online), or any other reproductions of similar nature. Online available from Springer-Verlag LNCS series.