Monitor-based Testing of Network Protocol Implementations Using Symbolic Execution
Authors: 
Hooman Asadian, Paul Fiterau-Brostean, Bengt Jonsson, Konstantinos SagonasAuthors Info & Claims
Hooman Asadian, Paul Fiterau-Brostean, Bengt Jonsson, Konstantinos SagonasAuthors Info & ClaimsARES '24: Proceedings of the 19th International Conference on Availability, Reliability and Security
Article No.: 17, Pages 1 - 12
Abstract
Implementations of network protocols must conform to their specifications in order to avoid security vulnerabilities and interoperability issues. To detect errors, testing must investigate an implementation’s response to a wide range of inputs, including those that could be supplied by an attacker. This can be achieved by symbolic execution, but its application in testing network protocol implementations has so far been limited. One difficulty when testing such implementations is that the inputs and requirements for processing a packet depend on the sequence of previous packets. We present a novel technique to encode protocol requirements by monitors, and then employ symbolic execution to detect violations of these requirements in protocol implementations. A monitor is a component external to the SUT, that observes a sequence of packets exchanged between protocol parties, maintains information about the state of the interaction, and can thereby detect requirement violations. Using monitors, requirements for stateful network protocols can be tested with a wide variety of inputs, without intrusive modifications in the source code of the SUT. We have applied our technique on the most recent versions of several widely-used DTLS and QUIC protocol implementations, and have been able to detect twenty two previously unknown bugs in them, twenty one of which have already been fixed and the remaining one has been confirmed.
References
[1]
Anastasios Andronidis and Cristian Cadar. 2022. SnapFuzz: High-throughput Fuzzing of Network Applications. In 31st ACM SIGSOFT International Symposium on Software Testing and Analysis(ISSTA ’22). ACM, New York, NY, USA, 340–351. https://doi.org/10.1145/3533767.3534376
[2]
Cyrille Artho, Howard Barringer, Allen Goldberg, Klaus Havelund, Sarfraz Khurshid, Michael R. Lowry, Corina S. Pasareanu, Grigore Rosu, Koushik Sen, Willem Visser, and Richard Washington. 2005. Combining test case generation and runtime verification. Theor. Comput. Sci. 336, 2-3 (2005), 209–234. https://doi.org/10.1016/j.tcs.2004.11.007
[3]
Hooman Asadian, Paul Fiterău-Broştean, Bengt Jonsson, and Konstantinos Sagonas. 2022. Applying Symbolic Execution to Test Implementations of a Network Protocol Against its Specification. In IEEE Conference on Software Testing, Verification and Validation(ICST 2022). IEEE, 70–81. https://doi.org/10.1109/ICST53961.2022.00019
[4]
Hooman Asadian, Paul Fiterău-Broştean, Bengt Jonsson, and Konstantinos Sagonas. 2022. Replication Material for the ICST 2022 Paper: Applying Symbolic Execution to Test Implementations of a Network Protocol Against its Specification. https://doi.org/10.5281/zenodo.5929867
[5]
Hooman Asadian, Paul Fiterău-Broştean, Bengt Jonsson, and Konstantinos Sagonas. 2024. Replication material for the ARES 2024 paper: Monitor-based Testing of Network Protocol Implementations Using Symbolic Execution. https://doi.org/10.5281/zenodo.11945614
[6]
David A. Basin, Felix Klaedtke, Samuel Müller, and Eugen Zalinescu. 2015. Monitoring Metric First-Order Temporal Properties. J. ACM 62, 2 (2015), 15:1–15:45. https://doi.org/10.1145/2699444
[7]
Benjamin Beurdouche, Karthikeyan Bhargavan, Antoine Delignat-Lavaud, Cédric Fournet, Markulf Kohlweiss, Alfredo Pironti, Pierre-Yves Strub, and Jean Karim Zinzindohoue. 2017. A Messy State of the Union: Taming the Composite State Machines of TLS. Commun. ACM 60, 2 (Feb. 2017), 99–107. https://doi.org/10.1145/3023357
[8]
Cristian Cadar, Daniel Dunbar, and Dawson Engler. 2008. KLEE: Unassisted and Automatic Generation of High-Coverage Tests for Complex Systems Programs. In Proceedings of the 8th USENIX Conference on Operating Systems Design and Implementation (San Diego, California) (OSDI ’08). USENIX Association, Berkeley, CA, USA, 209–224. http://dl.acm.org/citation.cfm?id=1855741.1855756
[9]
Cristian Cadar and Koushik Sen. 2013. Symbolic execution for software testing: three decades later. Commun. ACM 56, 2 (2013), 82–90. https://doi.org/10.1145/2408776.2408795
[10]
Marco M. Carvalho, Jared DeMott, Richard Ford, and David A. Wheeler. 2014. Heartbleed 101. IEEE Secur. Priv. 12, 4 (2014), 63–67. https://doi.org/10.1109/MSP.2014.66
[11]
Ian Cassar, Adrian Francalanza, Luca Aceto, and Anna Ingólfsdóttir. 2017. A Survey of Runtime Monitoring Instrumentation Techniques. In Proceedings Second International Workshop on Pre- and Post-Deployment Verification Techniques, PrePost@iFM 2017 (Torino, Italy) (EPTCS, Vol. 254), Adrian Francalanza and Gordon J. Pace (Eds.). 15–28. https://doi.org/10.4204/EPTCS.254.2
[12]
Sze Yiu Chau, Omar Chowdhury, Md. Endadul Hoque, Huangyi Ge, Aniket Kate, Cristina Nita-Rotaru, and Ninghui Li. 2017. SymCerts: Practical Symbolic Execution for Exposing Noncompliance in X.509 Certificate Validation Implementations. In 2017 IEEE Symposium on Security and Privacy (San Jose, CA, USA) (SP 2017). IEEE Computer Society, 503–520. https://doi.org/10.1109/SP.2017.40
[13]
Sze Yiu Chau, Moosa Yahyazadeh, Omar Chowdhury, Aniket Kate, and Ninghui Li. 2019. Analyzing Semantic Correctness with Symbolic Execution: A Case Study on PKCS#1 v1.5 Signature Verification. In 26th Annual Network and Distributed System Security Symposium (San Diego, CA, USA) (NDSS 2019). The Internet Society. https://doi.org/10.14722/ndss.2019.23430
[14]
Chu Chen, Cong Tian, Zhenhua Duan, and Liang Zhao. 2018. RFC-directed differential testing of certificate validation in SSL/TLS implementations. In Proceedings of the 40th International Conference on Software Engineering (Gothenburg, Sweden) (ICSE 2018), Michel Chaudron, Ivica Crnkovic, Marsha Chechik, and Mark Harman (Eds.). ACM, 859–870. https://doi.org/10.1145/3180155.3180226
[15]
Vitaly Chipounov, Volodymyr Kuznetsov, and George Candea. 2012. The S2E Platform: Design, Implementation, and Applications. ACM Trans. Comput. Syst. 30, 1 (2012), 2:1–2:49. https://doi.org/10.1145/2110356.2110358
[16]
Tim Dierks and Eric Rescorla. 2008. The Transport Layer Security TLS Protocol Version 1.2. RFC 5246. http://www.rfc-editor.org/rfc/rfc5246.txt
[17]
Klaus Havelund and Doron Peled. 2018. Efficient Runtime Verification of First-Order Temporal Properties. In Model Checking Software - 25th International Symposium, SPIN 2018(LNCS, Vol. 10869), María-del-Mar Gallardo and Pedro Merino (Eds.). Springer, 26–47. https://doi.org/10.1007/978-3-319-94111-0_2
[18]
Janardhan Iyengar and Martin Thomson. 2021. QUIC: A UDP-Based Multiplexed and Secure Transport. RFC 9000., 151 pages. https://www.rfc-editor.org/rfc/rfc9000.txt
[19]
James C. King. 1976. Symbolic Execution and Program Testing. Commun. ACM 19, 7 (July 1976), 385–394. https://doi.org/10.1145/360248.360252
[20]
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 (Beijing, China) (SIGCOMM 2019). ACM, 227–240. https://doi.org/10.1145/3341302.3342087
[21]
Ruijie Meng, Zhen Dong, Jialin Li, Ivan Beschastnikh, and Abhik Roychoudhury. 2022. Linear-time Temporal Logic guided Greybox Fuzzing. In Proceedings of the 44th International Conference on Software Engineering(ICSE’ 22). ACM, New York, NY, USA, 1343–1355. https://doi.org/10.1145/3510003.3510082
[22]
Bodo Möller, Thai Duong, and Krzysztof Kotowicz. 2014. This POODLE bites: exploiting the SSL 3.0 fallback. https://www.openssl.org/ bodo/ssl-poodle.pdf
[23]
R. Moskowitz, P. Nikander, P. Jokela, and T. Henderson. 2008. Host Identity Protocol. RFC 5201. https://www.ietd.org/rfc/rfc5201.txt updated by RFC 6253.
[24]
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 (Oakland, CA, USA) (NSDI 15). USENIX Association, 485–498. https://www.usenix.org/conference/nsdi15/technical-sessions/presentation/pedrosa
[25]
Van-Thuam Pham, Marcel Böhme, and Abhik Roychoudhury. 2020. AFLNET: A Greybox Fuzzer for Network Protocols. In IEEE 13th International Conference on Software Testing, Validation and Verification(ICST 2020). IEEE, 460–465. https://doi.org/10.1109/ICST46399.2020.00062
[26]
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 (Heraklion, Greece) (EPIQ@CoNEXT 2018). ACM, 15–21. https://doi.org/10.1145/3284850.3284853
[27]
Eric Rescorla and Nagendra Modadugu. 2012. Datagram Transport Layer Security Version 1.2. RFC 6347., 32 pages. http://www.rfc-editor.org/rfc/rfc6347.txt
[28]
Raimondas Sasnauskas, Philipp Kaiser, Russ Lucas Jukic, and Klaus Wehrle. 2012. Integration testing of protocol implementations using symbolic distributed execution. In 20th IEEE International Conference on Network Protocols (Austin, TX, USA) (ICNP 2012). IEEE Computer Society, 1–6. https://doi.org/10.1109/ICNP.2012.6459940
[29]
Raimondas Sasnauskas, Olaf Landsiedel, Muhammad Hamad Alizai, Carsten Weise, Stefan Kowalewski, and Klaus Wehrle. 2010. KleeNet: Discovering Insidious Interaction Bugs in Wireless Sensor Networks Before Deployment. In Proceedings of the 9th International Conference on Information Processing in Sensor Networks (Stockholm, Sweden) (IPSN 2010). ACM, 186–196. https://doi.org/10.1145/1791212.1791235
[30]
Raimondas Sasnauskas, Jó Ágila Bitsch Link, Muhammad Hamad Alizai, and Klaus Wehrle. 2008. KleeNet: automatic bug hunting in sensor network applications. In Proceedings of the 6th International Conference on Embedded Networked Sensor Systems (Raleigh, NC, USA) (SenSys 2008). ACM, 425–426. https://doi.org/10.1145/1460412.1460485
[31]
Fred B. Schneider. 2000. Enforceable security policies. ACM Trans. Inf. Syst. Secur. 3, 1 (2000), 30–50. https://doi.org/10.1145/353323.353382
[32]
JaeSeung Song, Cristian Cadar, and Peter R. Pietzuch. 2014. SymbexNet: Testing Network Protocol Implementations with Symbolic Execution and Rule-Based Specifications. IEEE Trans. Software Eng. 40, 7 (2014), 695–709. https://doi.org/10.1109/TSE.2014.2323977
[33]
W. Richard Stevens. 1990. Unix network programming. Prentice Hall.
[34]
Sören Tempel, Vladimir Herdt, and Rolf Drechsler. 2023. Specification-based Symbolic Execution for Stateful Network Protocol Implementations in the IoT. IEEE Internet of Things Journal (2023). https://doi.org/10.1109/JIOT.2023.3236694
[35]
Shameng Wen, Qingkun Meng, Chao Feng, and Chaojing Tang. 2017. A model-guided symbolic execution approach for network protocol implementations and vulnerability detection. PloS one 12, 11 (2017), e0188229. https://doi.org/10.1371/journal.pone.0188229
[36]
Michał Zalewski. 2013. American Fuzzy Lop. http://lcamtuf.coredump.cx/afl/.
Index Terms
- Monitor-based Testing of Network Protocol Implementations Using Symbolic Execution
Index terms have been assigned to the content through auto-classification.
Recommendations
SMBugFinder: An Automated Framework for Testing Protocol Implementations for State Machine Bugs
ISSTA 2024: Proceedings of the 33rd ACM SIGSOFT International Symposium on Software Testing and AnalysisImplementations of stateful network protocols must keep track of the presence, order and type of exchanged messages. Any errors, so-called state machine bugs, can compromise security. SMBugFinder provides an automated framework for detecting these bugs ...
Interoperability-Guided Testing of QUIC Implementations using Symbolic Execution
EPIQ'18: Proceedings of the Workshop on the Evolution, Performance, and Interoperability of QUICThe main reason for the standardization of network protocols, like QUIC, is to ensure interoperability between implementations, which poses a challenging task. Manual tests are currently used to test the different existing implementations for ...
Computational verification of C protocol implementations by symbolic execution
CCS '12: Proceedings of the 2012 ACM conference on Computer and communications securityWe verify cryptographic protocols coded in C for correspondence properties with respect to the computational model of cryptography. The first step uses symbolic execution to extract a process calculus model from a C implementation of the protocol. The ...
Comments
Information & Contributors
Information
Published In
July 2024
2032 pages
ISBN:9798400717185
DOI:10.1145/3664476
Copyright © 2024 Owner/Author.
This work is licensed under a Creative Commons Attribution International 4.0 License.
Publisher
Association for Computing Machinery
New York, NY, United States
Publication History
Published: 30 July 2024
Check for updates
Author Tags
Qualifiers
- Research-article
- Research
- Refereed limited
Funding Sources
Conference
ARES 2024
ARES 2024: The 19th International Conference on Availability, Reliability and Security
July 30 - August 2, 2024
Vienna, Austria
Acceptance Rates
Overall Acceptance Rate 228 of 451 submissions, 51%
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- 0Total Citations
- 96Total Downloads
- Downloads (Last 12 months)96
- Downloads (Last 6 weeks)55
Reflects downloads up to 06 Oct 2024
Other Metrics
Citations
View Options
View options
View or Download as a PDF file.
PDFeReader
View online with eReader.
eReaderHTML Format
View this article in HTML Format.
HTML FormatGet Access
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in