SpecMon: Modular Black-Box Runtime Monitoring of Security Protocols

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 study. We also provide a soundness result for our algorithm that ensures it accepts only event streams that are valid according to the specification model.