Protocols to Code: Formal Verification of a Next-Generation Internet Router

TL;DR

This work tackles the problem of ensuring both the security of Internet routing and the correctness of router implementations by presenting the first comprehensive formal verification of an Internet router in the SCION architecture. The authors use the Igloo methodology to perform end-to-end verification: protocol properties are proven in Isabelle/HOL via refinement, and the resulting I/O specification is automatically linked to the production Go code verified by Gobra. The approach yields both protocol-level guarantees (path authorization, valley freedom, loop freedom) and code-level guarantees (memory safety, race freedom, termination, and operational correctness), even in the presence of a strong attacker model. The work uncovers design and implementation bugs, strengthens security properties, and demonstrates that complex, performance-oriented production code can be soundly verified, with broad implications for designing verifiable networking systems and handling continual evolution.

Abstract

We present the first formally-verified Internet router, which is part of the SCION Internet architecture. SCION routers run a cryptographic protocol for secure packet forwarding in an adversarial environment. We verify both the protocol's network-wide security properties and low-level properties of its implementation. More precisely, we develop a series of protocol models by refinement in Isabelle/HOL and we use an automated program verifier to prove that the router's Go code satisfies memory safety, crash freedom, freedom from data races, and adheres to the protocol model. Both verification efforts are soundly linked together. Our work demonstrates the feasibility of coherently verifying a critical network component from high-level protocol models down to performance-optimized production code, developed by an independent team. In the process, we uncovered critical bugs in both the protocol and its implementation, which were confirmed by the code developers, and we strengthened the protocol's security properties. This paper explains our approach, summarizes the main results, and distills lessons for the design and implementation of verifiable systems, for the handling of continuous changes, and for the verification techniques and tools employed.

Figures (6)

• Figure 1: Network topology example. Autonomous systems are linked hierarchically (arrows), except among cores ASes (bold). Dotted lines represent authorized path segments.
• Figure 2: Overview of our approach.
• Figure 3: A two-segment packet at hop E of the path D-A-E-H in \ref{['fig:overview']} (payload not shown). For up-segments, where $\textit{dir}{} = \mathsf{false}$, the meaning of $\textit{prev}$ and $\textit{next}$ is reversed. The first hop field's $\textit{prev}{}$ and the last hop field's $\textit{next}{}$ are empty ($\bot$). The current segment and hop field have bold frames.
• Figure 4: The specification of the function , consisting of memory safety (Lines \ref{['line:code-example:memory-pre']} and \ref{['line:code-example:memory-post']}), functional properties (Lines \ref{['line:code-example:function-pre']} and \ref{['line:code-example:function-post']}), termination (Line \ref{['line:code-example:termination']}), the I/O spec (Lines \ref{['line:code-example:io-pre']} and \ref{['line:code-example:io-post']}), and properties about the I/O abstract state (Lines \ref{['line:code-example:model-pre']} and \ref{['line:code-example:model-post']}). and declare pre- and post.conditions, resp.
• Figure 5: The core predicate of the I/O specification generated from our protocol model. The predicate includes permissions for all I/O operationsprescribed by the protocol model (we show only the permission here). The recursive predicate application shows how the position in the protocol () and the model state () are updated when an I/O operation is performed. Variable is existentially quantified.