SpecMon: Modular Black-Box Runtime Monitoring of Security Protocols
Pages 2741 - 2755
Abstract
This work addresses the verification gap between formal protocol specifications and their real-world implementations by monitoring compliance with formal specifications.
We achieve this by instrumenting the networking and cryptographic libraries used by applications to generate event streams, even without access to the source code. An efficient algorithm is then employed to match these event streams against valid traces defined in the formal specification. Unlike previous approaches, our algorithm is capable of handling non-determinism, allowing it to support multiple concurrent sessions. Furthermore, our method introduces minimal overhead, as demonstrated through experiments on the WireGuard userspace implementation and a case study based on prior work. Notably, we find that the reference Tamarin model for WireGuard requires only minor adjustments, such as defining wire formats and correcting small inaccuracies uncovered during our case study. Finally, we provide formal proofs of soundness and completeness for our algorithm, ensuring that it accepts only valid event streams according to the specification and guarantees that all such valid streams are recognized.
References
[1]
Mihhail Aizatulin, Andrew D. Gordon, and Jan Jurjens. 2012. Computational verification of C protocol implementations by symbolic execution. In Proceedings of the 2012 ACM Conference on Computer and Communications Security. New York, NY, USA, 712--723.
[2]
Mihhail Aizatulin, Andrew D. Gordon, and Jan Jurjens. 2011. Extracting and verifying cryptographic models from C protocol code by symbolic execution. In Proceedings of the 18th ACM Conference on Computer and Communications Security. New York, NY, USA, 331--340.
[3]
José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, and François Dupressoir. 2013. Certified computer-aided cryptography: efficient provably secure machine code from high-level implementations. In Proceedings of the 2013 ACM SIGSAC Conference on Computer & Communications Security. New York, NY, USA, (Nov. 4, 2013), 1217--1230.
[4]
Omar Alrawi et al. 2024. SoK: An essential guide for using malware sandboxes in security applications: Challenges, pitfalls, and lessons learned. (2024). arXiv: 2403.16304 [cs.CR].
[5]
M. Ammann, L. Hirschi, and S. Kremer. 2024. DY fuzzing: Formal dolev-yao models meet cryptographic protocol fuzz testing. In 2024 IEEE Symposium on Security and Privacy (SP). Los Alamitos, CA, USA, (May 2024), 99--99.
[6]
Linard Arquint, Felix A.Wolf, Joseph Lallemand, Ralf Sasse, Christoph Sprenger, Sven N. Wiesner, David Basin, and Peter Muller. 2022. Sound Verification of Security Protocols: From Design to Interoperable Implementations (extended version). (Dec. 8, 2022). arXiv: 2212.04171 [cs]. preprint.
[7]
Howard Barringer, Yliès Falcone, Klaus Havelund, Giles Reger, and David Rydeheard. 2012. Quantified event automata: Towards expressive and efficient runtime monitors. In FM 2012: Formal Methods. Berlin, Heidelberg, 68--84.
[8]
Karthikeyan Bhargavan, Cédric Fournet, and Andrew D. Gordon. 2010. Modular verification of security protocol code by typing. In Proceedings of the 37th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. New York, NY, USA, 445--456.
[9]
Karthikeyan Bhargavan, Antoine Delignat Lavaud, Cedric Fournet, Alfredo Pironti, and Pierre Yves Strub. 2014. Triple Handshakes and Cookie Cutters: Breaking and Fixing Authentication over TLS. In 2014 IEEE Symposium on Security and Privacy. 2014 IEEE Symposium on Security and Privacy (SP). San Jose, CA, (May 2014), 98--113.
[10]
Bruno Blanchet. 2001. An Efficient Cryptographic Protocol Verifier Based on Prolog Rules. In Computer Security Foundations Workshop, 82--96.
[11]
David Cadé and Bruno Blanchet. 2015. Proved generation of implementations from computationally secure protocol specifications. J. Comput. Secur., 3, 331--402.
[12]
Vincent Cheval, Steve Kremer, and Itsaka Rakotonirina. 2018. DEEPSEC: Deciding Equivalence Properties in Security Protocols Theory and Practice. In 2018 IEEE Symposium on Security and Privacy (SP). 2018 IEEE Symposium on Security and Privacy (SP). San Francisco, CA, (May 2018), 529--546.
[13]
Edmund Clarke, Orna Grumberg, Somesh Jha, Yuan Lu, and Helmut Veith. 2000. Counterexample-Guided Abstraction Refinement. In Computer Aided Verification. Berlin, Heidelberg, 154--169.
[14]
Cas Cremers, Charlie Jacomme, and Philip Lukert. 2023. Subterm-Based Proof Techniques for Improving the Automation and Scope of Security Protocol Analysis. In 2023 IEEE 36th Computer Security Foundations Symposium (CSF). 2023 IEEE 36th Computer Security Foundations Symposium (CSF). (July 2023), 200--213.
[15]
Cas Cremers, Benjamin Kiesl, and Niklas Medinger. 2020. A Formal Analysis of {IEEE} 802.11?s {WPA2}: Countering the Kracks Caused by Cracking the Counters. In 29th USENIX Security Symposium (USENIX Security 20), 1--17.
[16]
[SW] Frida Developers, Frida Instrumentation Toolkit 2024. url: https://frida .re/.
[17]
Yevgeniy Dodis, Ilya Mironov, and Noah Stephens-Davidowitz. 2016. Message Transmission with Reverse Firewalls?Secure Communication on Corrupted Machines. In Advances in Cryptology -- CRYPTO 2016. Berlin, Heidelberg, 341--372.
[18]
D. Dolev and A. Yao. 1983. On the security of public key protocols. IEEE Transactions on Information Theory, 2, (Mar. 1983), 198--208.
[19]
Jason A Donenfeld and Kevin Milner. 2017. Formal verification of the Wire-Guard protocol. Technical Report, Tech. Rep.
[20]
Jason A. Donenfeld. 2017. WireGuard: Next Generation Kernel Network Tunnel. In Proceedings 2017 Network and Distributed System Security Symposium. Network and Distributed System Security Symposium. San Diego, CA.
[21]
Changhua He, Mukund Sundararajan, Anupam Datta, Ante Derek, and John C. Mitchell. 2005. A modular correctness proof of IEEE 802.11i and TLS. In Proceedings of the 12th ACM Conference on Computer and Communications Security. CCS05: 12th ACM Conference on Computer and Communications Security 2005. Alexandria VA USA, (Nov. 7, 2005), 2--15.
[22]
Dongyun Jin, Patrick O'Neil Meredith, Choonghwan Lee, and Grigore Rosu. 2012. JavaMOP: Efficient parametric runtime monitoring framework. In 2012 34th International Conference on Software Engineering (ICSE). 2012 34th International Conference on Software Engineering (ICSE). (June 2012), 1427--1430.
[23]
Jan Jurjens. 2008. Using Interface Specifications for Verifying Crypto-protocol Implementations, 15.
[24]
Nadim Kobeissi, Karthikeyan Bhargavan, and Bruno Blanchet. 2017. Automated Verification for Secure Messaging Protocols and Their Implementations: A Symbolic and Computational Approach. In 2017 IEEE European Symposium on Security and Privacy (EuroS&P). 2017 IEEE European Symposium on Security and Privacy (EuroS&P). (Apr. 2017), 435--450.
[25]
Benjamin Lipp. 2022. Mechanized Cryptographic Proofs of Protocols and their Link with Verified Implementations.
[26]
Simon Meier, Benedikt Schmidt, Cas Cremers, and David Basin. 2013. The TAMARIN Prover for the Symbolic Analysis of Security Protocols. In Computer Aided Verification. Berlin, Heidelberg, 696--701.
[27]
Sebastian Mödersheim and Georgios Katsoris. 2014. A Sound Abstraction of the Parsing Problem. In 2014 IEEE 27th Computer Security Foundations Symposium. 2014 IEEE 27th Computer Security Foundations Symposium. (July 2014), 259--273.
[28]
Kevin Morio and Robert Künnemann. 2024. SpecMon: Modular Black-Box Runtime Monitoring of Security Protocols. Full version. (2024). arXiv: 2409.02918.
[29]
[SW] Kevin Morio and Robert Künnemann, SpecMon: Modular Black-Box Runtime Monitoring of Security Protocols (CCS '24 Artifact) Oct. 2024.
[30]
Faezeh Nasrabadi, Robert Künnemann, and Hamed Nemati. 2023. CryptoBap: A Binary Analysis Platform for Cryptographic Protocols. In Proceedings of the 2023 ACM SIGSAC Conference on Computer and Communications Security. New York, NY, USA, (Nov. 21, 2023), 1362--1376.
[31]
Alfredo Pironti and Jan Jürjens. 2010. Formally-based black-box monitoring of security protocols. In Engineering Secure Software and Systems. Berlin, Heidelberg, 79--95. [32] Nadia Polikarpova and Michal Moskal. 2012. Verifying implementations of security protocols by refinement. In Verified Software: Theories, Tools, Experiments. Berlin, Heidelberg, 50--65.
[32]
[SW] OpenSSL Project, OpenSSL 2024. url: https://www.openssl.org/. [34] Sylvain Ruhault, Pascal Lafourcade, and Dhekra Mahmoud. 2024. A Unified Symbolic Analysis of WireGuard. In Proceedings 2024 Network and Distributed System Security Symposium. Network and Distributed System Security Symposium. San Diego, CA, USA.
[33]
Rui Shu, Peipei Wang, Sigmund A Gorski Iii, Benjamin Andow, Adwait Nadkarni, Luke Deshotels, Jason Gionta, William Enck, and Xiaohui Gu. 2017. A Study of Security Isolation Techniques. ACM Comput. Surv., 3, (Sept. 30, 2017), 1--37.
[34]
Christoph Sprenger, Tobias Klenze, Marco Eilers, Felix A. Wolf, Peter Müller, Martin Clochard, and David Basin. 2020. Igloo: soundly linking compositional refinement and separation logic for distributed system verification. Proc. ACM Program. Lang., (Nov. 13, 2020), 1--31, OOPSLA, (Nov. 13, 2020).
[35]
Nikhil Swamy, Juan Chen, Cédric Fournet, Pierre-Yves Strub, Karthikeyan Bhargavan, and Jean Yang. 2011. Secure distributed programming with valuedependent types. In Proceedings of the 16th ACM SIGPLAN International Conference on Functional Programming. New York, NY, USA, (Sept. 19, 2011), 266--278.
[36]
Mark Vella, Christian Colombo, Robert Abela, and Peter 'pacek. 2021. RVTEE: secure cryptographic protocol execution based on runtime verification. J Comput Virol Hack Tech, 3, (Sept. 1, 2021), 229--248.
[37]
Adam Young and Moti Yung. 1996. The Dark Side of 'Black-Box' Cryptography or: ShouldWe Trust Capstone' In Advances in Cryptology ' CRYPTO '96. Berlin, Heidelberg, 89--103.
Index Terms
- SpecMon: Modular Black-Box Runtime Monitoring of Security Protocols
Recommendations
An Executable Specification Language for Planning Attacks to Security Protocols
CSFW '00: Proceedings of the 13th IEEE workshop on Computer Security FoundationsWe propose AL_SP, a Declarative Executable Specification Language for Planning Attacks to Security Protocols based on logic programming. In AL_SP, we can give a declarative specification of a protocol with the natural semantics of send and receive ...
Security protocols analysis: A SDL-based approach
Organizations need to develop formally analyzed systems in order to achieve well-known formal method benefits. In order to study the security of communication systems, we have developed a methodology for the application of the formal analysis techniques,...
Stepwise development of security protocols: a speech act-oriented approach
FMSE '04: Proceedings of the 2004 ACM workshop on Formal methods in security engineeringWe propose a novel multi-layers paradigm for the design of key exchange protocols. In the top layer, protocols are specified in a high-level, declarative, formal language using speech acts as the basic building blocks. The declarative semantics of ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
December 2024
5188 pages
ISBN:9798400706363
DOI:10.1145/3658644
- General Chairs:
- Bo Luo,
- Xiaojing Liao,
- Jun Xu,
- Program Chairs:
- Engin Kirda,
- David Lie
Copyright © 2024 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 the author(s) 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
Publisher
Association for Computing Machinery
New York, NY, United States
Publication History
Published: 09 December 2024
Check for updates
Badges
Author Tags
Qualifiers
- Research-article
Conference
CCS '24
Sponsor:
CCS '24: ACM SIGSAC Conference on Computer and Communications Security
October 14 - 18, 2024
UT, Salt Lake City, USA
Acceptance Rates
Overall Acceptance Rate 1,261 of 6,999 submissions, 18%
Upcoming Conference
CCS '25
- Sponsor:
- sigsac
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- 0Total Citations
- 96Total Downloads
- Downloads (Last 12 months)96
- Downloads (Last 6 weeks)27
Reflects downloads up to 27 Feb 2025
Other Metrics
Citations
View Options
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in