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

TL;DR

This paper presents the first formally-verified Internet router within the SCION architecture, demonstrating the feasibility of verifying network components from high-level models to optimized code, and uncovering critical bugs in the process.

Contribution

It develops a comprehensive verification approach linking protocol models to implementation, and verifies a real-world router, setting a precedent for verifiable network infrastructure.

Findings

Verified security and low-level properties of the router

Uncovered and confirmed critical bugs in protocol and implementation

Strengthened the protocol's security properties

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.