research-article

Prognosis: closed-box analysis of network protocol implementations

Authors:

Tiago Ferreira,

Harrison Brewton,

Loris D'Antoni,

Alexandra SilvaAuthors Info & Claims

SIGCOMM '21: Proceedings of the 2021 ACM SIGCOMM 2021 Conference

Pages 762 - 774

https://doi.org/10.1145/3452296.3472938

Published: 09 August 2021 Publication History

Abstract

We present Prognosis, a framework offering automated closed-box learning and analysis of models of network protocol implementations. Prognosis can learn models that vary in abstraction level from simple deterministic automata to models containing data operations, such as register updates, and can be used to unlock a variety of analysis techniques -- model checking temporal properties, computing differences between models of two implementations of the same protocol, or improving testing via model-based test generation. Prognosis is modular and easily adaptable to different protocols (e.g. TCP and QUIC) and their implementations. We use Prognosis to learn models of (parts of) three QUIC implementations -- Quiche (Cloudflare), Google QUIC, and Facebook mvfst -- and use these models to analyse the differences between the various implementations. Our analysis provides insights into different design choices and uncovers potential bugs. Concretely, we have found critical bugs in multiple QUIC implementations, which have been acknowledged by the developers.

Supplementary Material

liu-public-review (666-public-review.pdf)

Prognosis: Closed-Box Analysis of Network Protocol Implementations: Public Review

Download
68.80 KB

Supplementary materials (PROGNOSIS.zip)

Download
470.51 MB

MP4 File (video-long.mp4)

Long Version Video

Download
1150.43 MB

MP4 File (video-presentation.mp4)

Conference Presentation Video

Download
749.68 MB

References

[1]

2021. cloudflare/quiche. (Jan. 2021). https://github.com/cloudflare/quiche original-date: 2018-09-29T18:22:05Z.

[2]

2021. facebookincubator/mvfst. (Jan. 2021). https://github.com/facebookincubator/mvfst original-date: 2018-04-09T22:49:15Z.

[3]

2021. Google QUIC - The Chromium Projects. (Jan. 2021). https://www.chromium.org/quic

[4]

2021a. Heartbleed - CVE-2014-0160. (Jan. 2021). https://nvd.nist.gov/vuln/detail/CVE-2014-0160

[5]

2021b. Let server abort on post-Retry packet number reset by dtikhonov · Pull Request #3990 · quicwg/base-drafts. (Jan. 2021). https://github.com/quicwg/base-drafts/pull/3990 Library Catalog: github.com.

[6]

2021c. NVD - CVE-2017-1000253. (Jan. 2021). https://nvd.nist.gov/vuln/detail/CVE-2017-1000253

[7]

2021d. NVD - CVE-2018-5390. (Jan. 2021). https://nvd.nist.gov/vuln/detail/CVE-2018-5390

[8]

2021e. Scapy. (Jan. 2021). https://scapy.net/

[9]

F. Aarts, J. De Ruiter, and E. Poll. 2013. Formal Models of Bank Cards for Free. In 2013 IEEE Sixth International Conference on Software Testing, Verification and Validation Workshops. 461--468.

Digital Library

[10]

Fides Aarts, Julien Schmaltz, and Frits Vaandrager. 2010. Inference and Abstraction of the Biometric Passport. In Leveraging Applications of Formal Methods, Verification, and Validation (Lecture Notes in Computer Science), Tiziana Margaria and Bernhard Steffen (Eds.). Springer, Berlin, Heidelberg, 673--686.

[11]

Dana Angluin. 1987. Learning regular sets from queries and counterexamples. Information and Computation 75, 2 (Nov. 1987), 87--106. 0890-5401

Digital Library

[12]

George Argyros, Ioannis Stais, Suman Jana, Angelos D. Keromytis, and Aggelos Kiayias. 2016. SFADiff: Automated Evasion Attacks and Fingerprinting Using Black-Box Differential Automata Learning. In Proceedings of the 2016 ACM SIGSAC Conference on Computer and Communications Security (CCS '16). Association for Computing Machinery, New York, NY, USA, 1690?1701.

Digital Library

[13]

Borja Balle and Mehryar Mohri. 2015. Learning Weighted Automata. In Algebraic Informatics - 6th International Conference, CAI 2015, Stuttgart, Germany, September 1-4, 2015. Proceedings (Lecture Notes in Computer Science), Andreas Maletti (Ed.), Vol. 9270. Springer, 1--21.

[14]

Karthikeyan Bhargavan et al. 2016. Everest: Towards a Verified, Drop-in Replacement of HTTPS. (2016), 11.

[15]

Steve Bishop, Matthew Fairbairn, Hannes Mehnert, Michael Norrish, Tom Ridge, Peter Sewell, Michael Smith, and Keith Wansbrough. 2019. Engineering with Logic: Rigorous Test-Oracle Specification and Validation for TCP/IP and the Sockets API. J. ACM 66, 1 (2019), 1:1--1:77.

Digital Library

[16]

Leonardo de Moura and Nikolaj Bjørner. 2008. Z3: An Efficient SMT Solver. In Tools and Algorithms for the Construction and Analysis of Systems (Lecture Notes in Computer Science), C. R. Ramakrishnan and Jakob Rehof (Eds.). Springer, Berlin, Heidelberg, 337--340.

[17]

Joeri de Ruiter. 2016. A Tale of the OpenSSL State Machine: A Large-Scale Black-Box Analysis. In Secure IT Systems - 21st Nordic Conference, NordSec 2016, Oulu, Finland, November 2-4, 2016, Proceedings (Lecture Notes in Computer Science), Billy Bob Brumley and Juha Röning (Eds.), Vol. 10014. 169--184.

[18]

Joeri de Ruiter and Erik Poll. 2015. Protocol State Fuzzing of TLS Implementations. In 24th USENIX Security Symposium, USENIX Security 15, Washington, D.C., USA, August 12-14, 2015, Jaeyeon Jung and Thorsten Holz (Eds.). USENIX Association, 193--206.

[19]

Antoine Delignat-Lavaud, Cédric Fournet, Bryan Parno, Jonathan Protzenko, Tahina Ramananandro, Jay Bosamiya, Joseph Lallemand, Itsaka Rakotonirina, and Yi Zhou. [n. d.]. A Security Model and Fully Verified Implementation for the IETF QUIC Record Layer. ([n. d.]), 17.

[20]

Antoine Delignat-Lavaud, Cédric Fournet, Bryan Parno, Jonathan Protzenko, Tahina Ramananandro, Jay Bosamiya, Joseph Lallemand, Itsaka Rakotonirina, and Yi Zhou. 2020. A Security Model and Fully Verified Implementation for the IETF QUIC Record Layer. IACR Cryptol. ePrint Arch. 2020 (2020), 114. https://eprint.iacr.org/2020/114

[21]

Paul Fiterau-Brostean, Bengt Jonsson, Robert Merget, Joeri de Ruiter, Konstantinos Sagonas, and Juraj Somorovsky. 2020. Analysis of {DTLS} Implementations Using Protocol State Fuzzing. 2523--2540. https://www.usenix.org/conference/usenixsecurity20/presentation/fiterau-brostean

[22]

Paul Fiterău-Broştean, Ramon Janssen, and Frits Vaandrager. 2016. Combining Model Learning and Model Checking to Analyze TCP Implementations. In Computer Aided Verification (Lecture Notes in Computer Science), Swarat Chaudhuri and Azadeh Farzan (Eds.). Springer International Publishing, Cham, 454--471.

[23]

Vidhi Goel, Rui Paulo, and Christoph Paasch. 2020. Testing QUIC with packetdrill. In Proceedings of the Workshop on the Evolution, Performance, and Interoperability of QUIC. ACM, Virtual Event USA, 1--7.

Digital Library

[24]

Harry B. Hunt and Daniel J. Rosenkrantz. 1977. On Equivalence and Containment Problems for Formal Languages. J. ACM 24, 3 (July 1977), 387--396. 0004-5411

Digital Library

[25]

Malte Isberner, Falk Howar, and Bernhard Steffen. 2015. The Open-Source LearnLib - A Framework for Active Automata Learning. In Computer Aided Verification - 27th International Conference, CAV 2015, San Francisco, CA, USA, July 18-24, 2015, Proceedings, Part I (Lecture Notes in Computer Science), Daniel Kroening and Corina S. Pasareanu (Eds.), Vol. 9206. Springer, 487--495.

[26]

William M McKeeman. 1998. Differential Testing for Software. 10, 1 (1998), 8.

[27]

Kenneth L. McMillan and Lenore D. Zuck. 2019. Formal specification and testing of QUIC. In Proceedings of the ACM Special Interest Group on Data Communication (SIGCOMM '19). Association for Computing Machinery, Beijing, China, 227--240.

Digital Library

[28]

Maxime Piraux, Quentin De Coninck, and Olivier Bonaventure. 2018. Observing the Evolution of QUIC Implementations. Proceedings of the Workshop on the Evolution, Performance, and Interoperability of QUIC (Dec. 2018), 8--14. arXiv: 1810.09134.

Digital Library

[29]

J. Postel. 1980. DoD standard Transmission Control Protocol. (1980). 2070-1721 https://www.rfc-editor.org/info/rfc0761 Number: RFC 761.

[30]

Felix Rath, Daniel Schemmel, and Klaus Wehrle. 2018. Interoperability-Guided Testing of QUIC Implementations Using Symbolic Execution. In Proceedings of the Workshop on the Evolution, Performance, and Interoperability of QUIC (EPIQ'18). Association for Computing Machinery, New York, NY, USA, 15?21.

Digital Library

[31]

Martin Thomson and Jana Iyengar. [n. d.]. QUIC: A UDP-Based Multiplexed and Secure Transport. ([n. d.]). https://tools.ietf.org/html/draft-ietf-quic-transport-29 Library Catalog: tools.ietf.org.

[32]

Frits Vaandrager. 2017. Model learning. Commun. ACM 60, 2 (Jan. 2017), 86--95. 0001-0782

Digital Library

[33]

Gerco van Heerdt, Clemens Kupke, Jurriaan Rot, and Alexandra Silva. 2020. Learning Weighted Automata over Principal Ideal Domains. In Foundations of Software Science and Computation Structures - 23rd International Conference, FOSSACS 2020 (Lecture Notes in Computer Science), Jean Goubault-Larrecq and Barbara König (Eds.), Vol. 12077. Springer, 602--621.

Digital Library

Cited By

Rohl ARoughan MWhite MChambers ASekar VYu MSeneviratne AVeitch D(2024)POSTER: Packet Field Tree: a hybrid approach, open database and evaluation methodology for Automated Protocol Reverse-EngineeringProceedings of the ACM SIGCOMM 2024 Conference: Posters and Demos10.1145/3672202.3673718(13-15)Online publication date: 4-Aug-2024
https://dl.acm.org/doi/10.1145/3672202.3673718
Fiterău-Broştean PJonsson BSagonas KTåquist FChristakis MPradel M(2024)SMBugFinder: An Automated Framework for Testing Protocol Implementations for State Machine BugsProceedings of the 33rd ACM SIGSOFT International Symposium on Software Testing and Analysis10.1145/3650212.3685310(1866-1870)Online publication date: 11-Sep-2024
https://dl.acm.org/doi/10.1145/3650212.3685310
Zheng MShi QLiu XXu XYu LLiu CWei GZhang X(2024)ParDiff: Practical Static Differential Analysis of Network Protocol ParsersProceedings of the ACM on Programming Languages10.1145/36498548:OOPSLA1(1208-1234)Online publication date: 29-Apr-2024
https://dl.acm.org/doi/10.1145/3649854
Show More Cited By

Index Terms

Prognosis: closed-box analysis of network protocol implementations
1. Theory of computation
  1. Formal languages and automata theory
    1. Automata extensions
      1. Transducers
    2. Automata over infinite objects
  2. Logic

Recommendations

Prognosis of breast cancer using genetic programming
KES'10: Proceedings of the 14th international conference on Knowledge-based and intelligent information and engineering systems: Part IV

Worldwide, breast cancer is the second most common type of cancer after lung cancer and the fifth most common cause of cancer death. In 2004, breast cancer caused 519,000 deaths worldwide. In order to reduce the cancer deaths and thereby increasing the ...
Model learning and model checking of SSH implementations
SPIN 2017: Proceedings of the 24th ACM SIGSOFT International SPIN Symposium on Model Checking of Software

We apply model learning on three SSH implementations to infer state machine models, and then use model checking to verify that these models satisfy basic security properties and conform to the RFCs. Our analysis showed that all tested SSH server models ...
Learning-based symbolic assume-guarantee reasoning for Markov decision process by using interval Markov process

Many real-life critical systems are described with large models and exhibit both probabilistic and non-deterministic behaviour. Verification of such systems requires techniques to avoid the state space explosion problem. Symbolic model checking and ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

SIGCOMM '21: Proceedings of the 2021 ACM SIGCOMM 2021 Conference

August 2021

868 pages

ISBN:9781450383837

DOI:10.1145/3452296

General Chairs:
Fernando Kuipers
Delft University of Technology
,
Matthew Caesar
University of Illinois at Urbana-Champaign

Copyright © 2021 ACM.

Permission to make digital or hard copies of all or 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. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

SIGCOMM: ACM Special Interest Group on Data Communication

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 09 August 2021

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Badges

Author Tags

Qualifiers

Research-article

Funding Sources

ERC Consolidator Grant

Conference

SIGCOMM '21

Sponsor:

SIGCOMM

SIGCOMM '21: ACM SIGCOMM 2021 Conference

August 23 - 27, 2021

Virtual Event, USA

Acceptance Rates

Overall Acceptance Rate 462 of 3,389 submissions, 14%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

12
Total Citations
View Citations
654
Total Downloads

Downloads (Last 12 months)108
Downloads (Last 6 weeks)11

Reflects downloads up to 21 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Rohl ARoughan MWhite MChambers ASekar VYu MSeneviratne AVeitch D(2024)POSTER: Packet Field Tree: a hybrid approach, open database and evaluation methodology for Automated Protocol Reverse-EngineeringProceedings of the ACM SIGCOMM 2024 Conference: Posters and Demos10.1145/3672202.3673718(13-15)Online publication date: 4-Aug-2024
https://dl.acm.org/doi/10.1145/3672202.3673718
Fiterău-Broştean PJonsson BSagonas KTåquist FChristakis MPradel M(2024)SMBugFinder: An Automated Framework for Testing Protocol Implementations for State Machine BugsProceedings of the 33rd ACM SIGSOFT International Symposium on Software Testing and Analysis10.1145/3650212.3685310(1866-1870)Online publication date: 11-Sep-2024
https://dl.acm.org/doi/10.1145/3650212.3685310
Zheng MShi QLiu XXu XYu LLiu CWei GZhang X(2024)ParDiff: Practical Static Differential Analysis of Network Protocol ParsersProceedings of the ACM on Programming Languages10.1145/36498548:OOPSLA1(1208-1234)Online publication date: 29-Apr-2024
https://dl.acm.org/doi/10.1145/3649854
Moon SSrivastava MBieri YMartins RSekar V(2024)Pryde: A Modular Generalizable Workflow for Uncovering Evasion Attacks Against Stateful Firewall Deployments2024 IEEE Symposium on Security and Privacy (SP)10.1109/SP54263.2024.00144(4440-4458)Online publication date: 19-May-2024
https://doi.org/10.1109/SP54263.2024.00144
Subaveerapandiyan AMvula DAhmad NTaj AAhmed M(2024)Assessing AI literacy and attitudes among medical students: implications for integration into healthcare practiceJournal of Health Organization and Management10.1108/JHOM-04-2024-0154Online publication date: 28-Oct-2024
https://doi.org/10.1108/JHOM-04-2024-0154
Vaandrager FEbrahimi MBloem R(2024)Learning Mealy machines with one timerInformation and Computation10.1016/j.ic.2023.105013295:PAOnline publication date: 27-Feb-2024
https://dl.acm.org/doi/10.1016/j.ic.2023.105013
Krumrey MBainczyk AHowar FSteffen B(2024)Malwa: Learnability by DesignPrinciples of Verification: Cycling the Probabilistic Landscape10.1007/978-3-031-75778-5_4(66-88)Online publication date: 18-Nov-2024
https://doi.org/10.1007/978-3-031-75778-5_4
Dierl SFiterau-Brostean PHowar FJonsson BSagonas KTåquist F(2024)Scalable Tree-based Register Automata LearningTools and Algorithms for the Construction and Analysis of Systems10.1007/978-3-031-57249-4_5(87-108)Online publication date: 6-Apr-2024
https://dl.acm.org/doi/10.1007/978-3-031-57249-4_5
Naseredini ABerger MSammartino MXiong S(2023)ALARM: Active LeArning of Rowhammer MitigationsProceedings of the 11th International Workshop on Hardware and Architectural Support for Security and Privacy10.1145/3569562.3569563(1-9)Online publication date: 21-Sep-2023
https://doi.org/10.1145/3569562.3569563
Zhang JRen SDong EMeng ZYang YXu MYang SZhang MYue Y(2023)Reducing Mobile Web Latency Through Adaptively Selecting Transport ProtocolIEEE/ACM Transactions on Networking10.1109/TNET.2023.323590731:5(2162-2177)Online publication date: 31-Jan-2023
https://dl.acm.org/doi/10.1109/TNET.2023.3235907
Show More Cited By

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents