SpecMon: Modular Black-Box Runtime Monitoring of Security Protocols

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.