Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

SpecMon: Modular Black-Box Runtime Monitoring of Security Protocols

Kevin Morio, Robert Künnemann

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.

SpecMon: Modular Black-Box Runtime Monitoring of Security Protocols

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.
Paper Structure (57 sections, 12 theorems, 65 equations, 4 figures, 2 tables, 4 algorithms)

This paper contains 57 sections, 12 theorems, 65 equations, 4 figures, 2 tables, 4 algorithms.

Table of Contents

  1. Introduction
  2. Contributions
  3. Outline
  4. Related Work
  5. Architecture Overview
  6. Event Aggregator
  7. Aggregation Assumption
  8. Cryptographic operations
  9. Network communication
  10. Environment interface
  11. Syntax and Informal Semantics of Program Events
  12. Mode of Integration
  13. Binary instrumentation
  14. Annotated libraries
  15. Verifiable secure closed-source software by isolation
  16. ...and 42 more sections

Key Result

theorem 1

Let $t$ be a likely event stream and $\mathcal{R}$ a set of eMSRs. If $t' \in M(\mathcal{R}, t)$, then there exists an abstraction function $\alpha \colon \mathbb{B}^* \to \mathcal{M}\xspace$ and a symbolic trace $t^* \in \mathit{traces}\xspace(\mathcal{R})$, such that $\alpha(t) =_E\xspace t^*|_\ma

Figures (4)

  • Figure 1: Architecture overview
  • Figure 2: The set of message deduction rules MD.
  • Figure 3: with format strings from SimpleMAC
  • Figure 4: Evaluation results for SimpleMAC (left) and WireGuard (right)

Theorems & Definitions (39)

  • example 1
  • definition 1: Executions and Traces
  • example 2
  • example 3
  • definition 2: Split Rule (simplified)
  • example 4
  • example 5
  • definition 3: Extended MSRs
  • definition 4: Trace Rewriting
  • definition 5: Monitor Output
  • ...and 29 more