Kenneth L. McMillan
ABSTRACT
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.
Supplemental Material
- Rajeev Alur, Pavol Černý, P. Madhusudan, and Wonhong Nam. 2005. Synthesis of interface specifications for Java classes. In Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2005, Long Beach, California, USA, January 12-14, 2005. ACM, 98--109. Google Scholar
Digital Library
- Clark W. Barrett, Roberto Sebastiani, Sanjit A. Seshia, and Cesare Tinelli. 2009. Satisfiability Modulo Theories. In Handbook of Satisfiability, Armin Biere, Marijn Heule, Hans van Maaren, and Toby Walsh (Eds.). Frontiers in Artificial Intelligence and Applications, Vol. 185. IOS Press, 825--885.Google Scholar
- Benjamin Beurdouche, Karthikeyan Bhargavan, Antoine Delignat-Lavaud, Cédric Fournet, Markulf Kohlweiss, Alfredo Pironti, Pierre-Yves Strub, and Jean Karim Zinzindohoue. 2015. A Messy State of the Union: Taming the Composite State Machines of TLS. In 2015 IEEE Symposium on Security and Privacy, SP 2015, San Jose, CA, USA, May 17-21, 2015. IEEE Computer Society, 535--552. Google ScholarDigital Library
- Karthikeyan Bhargavan, Cédric Fournet, Markulf Kohlweiss, Alfredo Pironti, and Pierre-Yves Strub. 2013. Implementing TLS with Verified Cryptographic Security. In 2013 IEEE Symposium on Security and Privacy, SP 2013, Berkeley, CA, USA, May 19-22, 2013. IEEE, 445--459. Google ScholarDigital Library
- Steve Bishop, Matthew Fairbairn, Hannes Mehnert, Michael Norrish, Tom Ridge, Peter Sewell, Michael Smith, and Keith Wansbrough. 2018. Engineering with Logic: Rigorous Test-Oracle Specification and Validation for TCP/IP and the Sockets API. JACM 1, 66 (12 2018), 1--77. Google ScholarDigital Library
- Robert S. Boyer, Bernard Elspas, and Karl N. Levitt. 1975. SELECT-a formal system for testing and debugging programs by symbolic execution. In Proceedings of the International Conference on Reliable Software. ACM, 234--245. Google ScholarDigital Library
- Josip Bozic, Lina Marsso, Radu Mateescu, and Franz Wotawa. 2018. A Formal TLS Handshake Model in LNT. In Proceedings Third Workshop on Models for Formal Analysis of Real Systems and Sixth International Workshop on Verification and Program Transformation, MARS/VPT@ETAPS 2018, and Sixth International Workshop on Verification and Program Transformation, Thessaloniki, Greece, 20th April 2018. To be published in EPCT, 1--40.Google Scholar
- Cristian Cadar, Daniel Dunbar, and Dawson R. Engler. 2008. KLEE: Unassisted and Automatic Generation of High-Coverage Tests for Complex Systems Programs. In 8th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2008, December 8-10, 2008, San Diego, California, USA, Proceedings. USENIX Association, 209--224. Google ScholarDigital Library
- Chia Yuan Cho, Domagoj Babic, Eui Chul Richard Shin, and Dawn Song. 2010. Inference and analysis of formal models of botnet command and control protocols. In Proceedings of the 17th ACM Conference on Computer and Communications Security, CCS 2010, Ehab Al-Shaer, Angelos D. Keromytis, and Vitaly Shmatikov (Eds.). ACM, 426--439. Google ScholarDigital Library
- Andrey Chudnov, Nathan Collins, Byron Cook, Joey Dodds, Brian Huffman, Colm MacCárthaigh, Stephen Magill, Eric Mertens, Eric Mullen, Serdar Tasiran, Aaron Tomb, and Eddy Westbrook. 2018. Continuous Formal Verification of Amazon s2n. In Computer Aided Verification - 30th International Conference Part II, Vol. 10982. Springer, 430--446.Google Scholar
- Koen Claessen, Colin Runciman, Olaf Chitil, John Hughes, and Malcolm Wallace. 2002. Testing and Tracing Lazy Functional Programs Using QuickCheck and Hat. In Advanced Functional Programming, 4th International School, AFP 2002, Oxford, UK, August 19-24, 2002, Revised Lectures, Vol. 2638. Springer, 59--99.Google Scholar
- The Mitre Corporation. 2014. CVE-2014-0160. https://cve.mitre.org/cgi-bin/cvename.cgi?name=CVE-2014-0160.Google Scholar
- The Mitre Corporation. 2014. CVE-2014-3566. https://cve.mitre.org/cgi-bin/cvename.cgi?name=CVE-2014-3566.Google Scholar
- Cas Cremers, Marko Horvat, Jonathan Hoyland, Sam Scott, and Thyla van der Merwe. 2017. A Comprehensive Symbolic Analysis of TLS 1.3. In Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security, CCS 2017, Dallas, TX, USA, October 30 - November 03, 2017, Bhavani M. Thuraisingham, David Evans, Tal Malkin, and Dongyan Xu (Eds.). ACM, 1773--1788. Google ScholarDigital Library
- Edsger W. Dijkstra. 1975. Guarded Commands, Nondeterminacy and Formal Derivation of Programs. Commun. ACM 18, 8 (1975), 453--457. Google ScholarDigital Library
- Dimitra Giannakopoulou, Corina S. Pasareanu, and Colin Blundell. 2008. Assume-guarantee testing for software components. IET Software 2, 6 (2008), 547--562.Google ScholarCross Ref
- Internet-Draft. 2019. QUIC: A UDP-Based Multiplexed and Secure Transport (Version 18). https://tools.ietf.org/id/draft-ietf-quic-transport-18.Google Scholar
- Internet-Draft. 2019. QUIC: QUIC Loss Detection and Congestion Control. https://tools.ietf.org/html/draft-ietf-quic-recovery-18.Google Scholar
- James E. Johnson, David E. Langworthy, Leslie Lamport, and Friedrich H. Vogt. 2007. Formal specification of a Web services protocol. J. Log. Algebr. Program. 70, 1 (2007), 34--52.Google ScholarCross Ref
- Hyojeong Lee, Jeff Seibert, Dylan Fistrovic, Charles Edwin Killian, and Cristina Nita-Rotaru. 2015. Gatling: Automatic Performance Attack Discovery in Large-Scale Distributed Systems. ACM Trans. Inf. Syst. Secur. 17, 4 (2015), 13:1--13:34. Google ScholarDigital Library
- Kenneth L. McMillan. 2016. Modular specification and verification of a cache-coherent interface. In 2016 Formal Methods in Computer-Aided Design, FMCAD 2016, Mountain View, CA, USA, October 3-6, 2016. IEEE, 109--116. Google ScholarDigital Library
- Kenneth L. McMillan. 2019. Mechanized Specification of QUIC. https://github.com/microsoft/ivy/tree/master/doc/examples/quic.Google Scholar
- Kenneth L. McMillan. Last updated 2019. Ivy. http://microsoft.github.io/ivy.Google Scholar
- K. L. McMillan and L. D. Zuck. 2019. Compositional Testing of Network Protocols. http://mcmil.net/pubs/SECDEV19.pdf. In IEEE Secure Development Conference (SecDev 2019). To appear.Google Scholar
- Rashmi Mudduluru, Pantazis Deligiannis, Ankush Desai, Akash Lal, and Shaz Qadeer. 2017. Lasso detection using partial-state caching. In 2017 Formal Methods in Computer Aided Design, FMCAD 2017, Vienna, Austria, October 2-6, 2017. 84--91. Google ScholarDigital Library
- B. Neelakantan and S. V.Raghavan. 1995. Protocol Conformance Testing - A Survey. In Computer Networks, Architecture and Applications, S. V. Raghavan et al. (Ed.). Springer, Chapter 1, 175--191.Google Scholar
- Oded Padon, Kenneth L. McMillan, Aurojit Panda, Mooly Sagiv, and Sharon Shoham. 2016. Ivy: safety verification by interactive generalization. In Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2016, Santa Barbara, CA, USA, June 13-17, 2016. ACM, 614--630. Google ScholarDigital Library
- Javier Paris and Thomas Arts. 2009. Automatic testing of TCP/IP implementations using QuickCheck. In Proceedings of the 8th ACM SIGPLAN Workshop on Erlang, Edinburgh, Scotland, UK, September 5, 2009. ACM, 83--92. Google ScholarDigital Library
- Luis Pedrosa, Ari Fogel, Nupur Kothari, Ramesh Govindan, Ratul Mahajan, and Todd D. Millstein. 2015. Analyzing Protocol Implementations for Interoperability. In 12th USENIX Symposium on Networked Systems Design and Implementation, NSDI 15, Oakland, CA, USA, May 4-6, 2015. USENIX Association, 485--498. https://www.usenix.org/conference/nsdi15/technical-sessions/presentation/pedrosa Google ScholarDigital Library
- Erik Poll, Joeri de Ruiter, and Aleksy Schubert. 2015. Protocol State Machines and Session Languages: Specification, implementation, and Security Flaws. In 2015 IEEE Symposium on Security and Privacy Workshops, SPW 2015, San Jose, CA, USA, May 21-22, 2015. IEEE, 125--133. Google ScholarDigital Library
- Abdullah Rasool, Greg Alpár, and Joeri de Ruiter. 2019. State machine inference of QUIC. CoRR abs/1903.04384 (2019). arXiv:1903.04384 http://arxiv.org/abs/1903.04384Google Scholar
- Felix Rath, Daniel Schemmel, and Klaus Wehrle. 2018. Interoperability-Guided Testing of QUIC Implementations using Symbolic Execution. In Workshop on the Evolution, Performance, and Interoperability of QUIC (EPIQ 2018). ACM, 15--21. Google ScholarDigital Library
- Ivan Ristic. 2014. POODLE Bites TLS. https://blog.qualys.com/ssllabs/2014/12/08/poodle-bites-tls.Google Scholar
- Jan Rüth. 2018. How much of the Internet is using QUIC? https://blog.apnic.net/2018/05/15/how-much-of-the-internet-is-using-quic/.Google Scholar
- Margus Veanes, Colin Campbell, Wolfgang Grieskamp, Wolfram Schulte, Nikolai Tillmann, and Lev Nachmanson. 2008. Model-Based Testing of Object-Oriented Reactive Systems with Spec Explorer. Lecture Notes in Computer Science, Vol. 4949. Springer Verlag, 39--76. Google ScholarDigital Library
- Gregor von Bochmann. 1989. Protocol Specification for OSI. Computer Networks and ISDN Systems 18, 3 (1989), 167--184. Google ScholarDigital Library
- QUIC working group. 2019. QUIC Working Group. https://quicwg.org/.Google Scholar
- Pamela Zave. 2015. How to Make Chord Correct (Using a Stable Base). CoRR abs/1502.06461 (2015). http://arxiv.org/abs/1502.06461Google Scholar
Recommendations
Multipath QUIC: Design and Evaluation
CoNEXT '17: Proceedings of the 13th International Conference on emerging Networking EXperiments and TechnologiesQuick UDP Internet Connection (QUIC) is a recent protocol initiated by Google that combines the functions of HTTP/2, TLS, and TCP directly over UDP, with the goal to reduce the latency of client-server communication. It can replace the traditional HTTP/...
Formal specification-based conformance testing
The paper discusses the use of formal specifications for conformance testing of OSI protocols and divides the discussion in two parts: test design and tester design. A draft standard formal specification of the Class 4 transport protocol in Estelle is ...
Formal specification-based conformance testing
SIGCOMM '86: Proceedings of the ACM SIGCOMM conference on Communications architectures & protocolsThe paper discusses the use of formal specifications for conformance testing of OSI protocols and divides the discussion in two parts: test design and tester design. A draft standard formal specification of the Class 4 transport protocol in Estelle is ...
Comments