QUIC is a new Internet secure transport protocol currently
in the process of IETF standardization. It is intended as a
replacement for the TLS/TCP stack and will be the basis of
HTTP/3, the next official version of the hypertext transfer
protocol. As a result, it is likely, in the near future, to carry
a substantial fraction of traffic on the Internet. We describe
our experience applying a methodology of compositional
specification-based testing to QUIC. We develop a formal
specification of the wire protocol, and use this specification
to generate automated randomized testers for implementations of QUIC. The testers effectively take one role of the
QUIC protocol, interacting with the other role to generate
full protocol executions, and verifying that the implementations conform to the formal specification. This form of testing
generates significantly more diverse stimuli and stronger correctness criteria than interoperability testing, the primary
method used to date to validate QUIC and its implementations. As a result, numerous implementation errors have
been found. These include some vulnerabilities at the protocol and implementation levels, such as an off-path denial
of service scenario and an information leak similar to the
“heartbleed” vulnerability in OpenSSL. TEST
Paper
Formal specification and testing of QUIC (Kenneth L. McMillan and Lenore D. Zuck), In Proceedings of ACM Special Interest Group on Data Communication (SIGCOMM’19), ACM, 2019. [bibtex] [pdf] [slides] video