SpecMon: Modular Black-Box Runtime Monitoring of Security Protocols
Kevin Morio, Robert K\"unnemann

TL;DR
SpecMon is a modular runtime monitoring system that verifies security protocol compliance by matching observed event streams to formal specifications, handling non-determinism and multiple sessions with low overhead.
Contribution
It introduces an efficient, non-intrusive algorithm for runtime monitoring of security protocols that can operate without source code access and handle complex session behaviors.
Findings
Successfully applied to WireGuard with minimal modifications
Achieves low runtime overhead in practical scenarios
Provides formal soundness guarantees for event stream validation
Abstract
There exists a verification gap between formal protocol specifications and their actual implementations, which this work aims to bridge via monitoring for compliance to the formal specification. We instrument the networking and cryptographic library the application uses to obtain a stream of events. This is possible even without source code access. We then use an efficient algorithm to match these observations to traces that are valid in the specification model. In contrast to prior work, our algorithm can handle non-determinism and thus, multiple sessions. It also achieves a low overhead, which we demonstrate on the WireGuard reference implementation and a case study from prior work. We find that the reference Tamarin model for WireGuard can be used with little change: We only need to specify wire formats and correct some small inaccuracies that we discovered while conducting the case…
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.
