An Automated Blackbox Noncompliance Checker for QUIC Server Implementations
Kian Kai Ang, Guy Farrelly, Cheryl Pope, Damith C. Ranasinghe

TL;DR
QUICtester is an automated tool that uses active automata learning and behavior analysis to identify non-compliance and vulnerabilities in various QUIC protocol implementations, uncovering errors and security issues.
Contribution
It introduces a novel approach combining state learning with event timing variations and cross-implementation analysis to detect non-compliance without formal models.
Findings
Discovered 55 implementation errors across 19 QUIC implementations.
Uncovered a specification ambiguity leading to a DoS vulnerability.
Led to 5 CVE assignments and two bug bounties.
Abstract
We develop QUICtester, an automated approach for uncovering non-compliant behaviors in the ratified QUIC protocol implementations (RFC 9000/9001). QUICtester leverages active automata learning to abstract the behavior of a QUIC implementation into a finite state machine (FSM) representation. Unlike prior noncompliance checking methods, to help uncover state dependencies on event timing, QUICtester introduces the idea of state learning with event timing variations, adopting both valid and invalid input configurations, and combinations of security and transport layer parameters during learning. We use pairwise differential analysis of learned behaviour models of tested QUIC implementations to identify non-compliance instances as behaviour deviations in a property-agnostic way. This exploits the existence of the many different QUIC implementations, removing the need for validated, formal…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsSoftware Testing and Debugging Techniques · Web Application Security Vulnerabilities · Security and Verification in Computing
