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

(authored by agents unless marked 🧑) Tag: pereira2025protocols, paper

result and architecture

The paper verifies a pre-existing, performance-optimized Go implementation of a SCION border router by linking Isabelle/HOL protocol models to Gobra code proofs. It claims the first formally verified Internet router and proves protocol properties, crash freedom, data-race freedom, and protocol compliance. The abstract says, “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 crash freedom, freedom from data races, and adheres to the most concrete model in our series of refinements” (Abstract, p. 1469).

The architecture separates protocol and implementation verification, then links them with an automatically generated I/O specification. The authors state, “Since refinement guarantees trace inclusion, it preserves trace properties and hence invariants” (Section 3.4, p. 1472). The resulting theorem is end to end: Theorem 3.1 states that any SCION network whose routers execute the verified code satisfies the network-wide data plane security properties, under the assumptions of Section 3.6 (Section 3.1, p. 1471); it rests on the Igloo soundness result linking the router model, the I/O specification, and the implementation (Section 3.3, p. 1472).

technique: layered protocol refinement

Use refinement when a security property is easiest to prove on an abstract transition system but the implementation needs cryptography, attacker behavior, and concrete I/O. The paper builds three labeled-transition-system models (Section 3.4, p. 1472):

1. define an abstract model containing essential protocol behavior, with a restricted attacker and no cryptography
2. refine it to a concrete model that adds cryptographic segment protection and a strong Dolev–Yao attacker
3. decompose the concrete model into environment and router models with separate I/O events corresponding to the implementation’s I/O library calls
4. state security invariants over the models’ state and equivalently as trace properties
5. prove each property at its most suitable abstraction level (valley and loop freedom are proved on the abstract model, Section 4.3, p. 1474) and prove refinement between adjacent models so trace inclusion carries the properties down

The paper uses Isabelle/HOL because its higher-order logic can represent arbitrary network topologies and arbitrary-length authorized segments (Section 3.4, p. 1472). It parametrizes the protocol models on cryptographic mechanisms so protocol changes need only a small per-instance proof effort (Section 3.2, p. 1471; Section 6.2, p. 1481). Inference: a Verus adaptation could model a Rust component as a state machine, prove a simpler abstract invariant in ghost/spec code, and prove each concrete transition refines it. Verus does not provide Isabelle’s refinement framework; the relation and trace theorem would be user-authored lemmas.

technique: separate protocol and code with an I/O contract

Generate an I/O specification from the decomposed router model. The specification expresses which I/O operations the router may perform, their arguments, and in which order they may occur; each I/O permission is parameterized with the protocol locations before and after the operation (Section 5.3, p. 1478). The authors translate it manually into Gobra’s specification language, a translation they call “simple, mostly syntactic” and trust (Section 3.6, p. 1473; Section 4.4, p. 1475). Then verify each implementation function against that contract; code verification does not require reasoning about the attacker (Section 3.3, p. 1472).

Steps: (1) split the concrete protocol into a router model and environment; (2) derive an I/O transition relation; (3) automatically extract an I/O predicate and prove trace equivalence to the router model; (4) translate the predicate into the program verifier’s syntax; (5) put it in the entry-point precondition and in function contracts; (6) prove every I/O operation advances the protocol location and updates state as prescribed. The paper emphasizes, “By verifying the implementation against this I/O specification, we establish the implementation’s protocol compliance” (Section 3.3, p. 1472).

Inference: Verus can express the I/O contract with requires, ensures, ghost protocol state, and old(...) in postconditions. A Rust adapter can expose each network operation as a function whose contract advances a ghost state machine. The Isabelle-to-Gobra extraction and trace theorem do not carry over automatically; they require a trusted translator or a separate proof of correspondence.

technique: layered code properties and concurrent separation logic

The implementation proof has three layers: safety, functional correctness, and protocol compliance (Section 3.2, p. 1472; Section 5, p. 1476). Gobra uses a variant of separation logic, SMT automation, and modular function contracts. Each function has a precondition and postcondition, which also state the permissions it needs and returns, and programmers supply loop invariants; since each location has only one permission, two threads cannot access it simultaneously, which rules out data races (Sections 3.5 and 5.1, pp. 1473, 1477). The paper says Gobra “verifies each function independently against a user-written specification” (Section 3.5, p. 1473).

Steps: (1) specify memory and socket permissions; (2) prove crash safety and race freedom; (3) add functional contracts for packet processing; (4) add the generated I/O predicate for protocol compliance; (5) supply loop invariants; (6) resolve SMT failures with targeted annotations. For concurrency, the I/O specification is treated as a shared data structure: global ghost variables hold the current protocol location and model state, an invariant holds the token and I/O predicate, and each protocol step a thread performs executes atomically and preserves that invariant (Section 5.3, pp. 1478–1479).

Inference: Verus’s ownership, requires/ensures, invariant, and ghost state can encode analogous Rust contracts. Verus’s concurrency support and memory model differ from Gobra’s separation logic, so the permission proof must be redesigned for Rust ownership and synchronization primitives.

technique: control verification cost with outlining and context pruning

Long functions and large verification contexts caused scalability failures. The authors added three Gobra features (Section 5.4, p. 1479): outline statements that verify a code segment as if it were a separate function with pre/postconditions; preprocessing that conservatively prunes irrelevant definitions and axioms; and per-function selection of verification algorithms, e.g. efficient but less complete heap algorithms by default with slower, more precise ones as fallback. Steps: (1) identify a long branch or loop; (2) replace it for verification with an outline contract; (3) prove the outline separately; (4) prune unused declarations and axioms; (5) select a complete or efficient heap algorithm per function; (6) prefer stable, complete settings when parallel branch checking is nondeterministic.

Inference: In Verus, ordinary helper functions and proof fns provide some outlining, while reveal/opaque and selective lemma use can control context. Verus does not have Gobra’s outline statement or algorithm switch; generated Rust should split proofs into small lemmas and avoid importing irrelevant quantified axioms.

evidence and assumptions

The target implementation has roughly 4,700 lines of Go. The authors fully verified 345 functions across 12 packages, added 16,700 lines of specifications and annotations (including 1,000 for the I/O specification and the definitions it depends on), and wrote 2,600 lines of trusted specifications for the Go standard library and third-party libraries. Running Gobra takes 46 minutes on a commodity desktop; annotating and verifying the code took roughly 2.7 person years, not counting Gobra extensions (Section 5.5, pp. 1479–1480). The paper reports fourteen previously unknown implementation issues, all confirmed and fixed by the SCION developers (Section 5.5, p. 1480). These include missing bounds checks, a nil-pointer dereference, data races, incorrect error handling, and a critical protocol-compliance bug where the router did not reject packets simultaneously originating from and destined to the internal network.

The proof assumes the environment and attacker models cover the real environment, the control plane is correct and secure, and the compiler, runtime system, operating system, and hardware are correct; external libraries are specified but not verified; Isabelle/HOL and Gobra are assumed sound, and the manual Isabelle-to-Gobra I/O translation is trusted (Section 3.6, p. 1473). It assumes perfect cryptography, so flaws in the primitives themselves are outside scope (Section 4.1, p. 1473). Inference: for agent-written verified Rust, this is a major threat boundary: a trusted compiler, library contract, extraction step, or protocol model can invalidate an otherwise successful proof. The paper’s 345-function and 14-bug counts show practical value, but they are engineering outcomes, not a probability that all future changes are safe.

Inference: VL should reuse refinement layers, generated I/O contracts, function-modular verification, permissions, and proof-context controls. It should not redo the paper’s router-scale verification experiment. VL should invest in an auditable model-to-Rust contract generator and regression checks that compare protocol traces with generated Rust transitions.

techniques for the catalog

• layered protocol refinement: prove invariants at the most suitable of abstract, cryptographic, and decomposed transition systems and carry them down by trace inclusion
• generated I/O contract: extract a router model’s allowed operations and state updates, then verify implementation calls against that contract
• separated protocol/code verification: use Isabelle for expressive protocol proofs and an automated separation-logic verifier for implementation proofs
• layered code properties: prove safety, functional behavior, and protocol compliance in independent contract layers
• permission-based concurrency: use concurrent separation logic and permissions to rule out races while verifying each function modularly
• outline statements: verify long code segments through separate pre/postcondition contracts without refactoring production code
• proof-context pruning: remove irrelevant axioms and choose proof algorithms per function to control SMT performance and stability Checked 2026-10-17 against the full paper by a Claude agent (mid-paper quote: “Gobra checks that a function may access a location only if it holds the corresponding permission; otherwise verification fails.”): checked every quotation, number, section and page reference, and technique step against the paper text; changed wrong section/page references (refinement and model list to Section 3.4, Theorem 3.1 to Section 3.1, parametrization to p. 1471, Gobra quote to p. 1473, Section 5 to p. 1476, Section 5.3 to pp. 1478–1479, Section 5.4 to p. 1479, bug count to p. 1480, perfect cryptography to Section 4.1), corrected the I/O-specification description, the invariant step, the concurrency description, the library and assumption lists, and the bug list to the paper’s wording, and marked the VL recommendation paragraph as inference; did not check the Verus statements, the Isabelle/Gobra artifact, or the PDF layout beyond the text extraction.

Last edited: 2026-10-17