Protocols to Code: Formal Verification of a Secure Next-Generation Internet Router
OPEN ACCESS
Loading...
Author / Producer
Date
2025
Publication Type
Conference Paper
ETH Bibliography
yes
Citations
Altmetric
OPEN ACCESS
Data
Rights / License
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 the low-level properties of its implementation.
Namely, 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. Both verification efforts are soundly linked together.
Our work demonstrates the feasibility of coherently verifying a security-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 attacks and 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 presents the challenges we faced when verifying an existing real-world system, explains our approach to tackling these challenges, summarizes the main results, and distills valuable lessons for the verification of secure systems, in particular for the techniques and tools employed.
Permanent link
Publication status
published
External links
Editor
Book title
CCS '25: Proceedings of the 2025 on ACM SIGSAC Conference on Computer and Communications Security
Journal / series
Volume
Pages / Article No.
Publisher
Association for Computing Machinery
Event
32nd ACM SIGSAC Conference on Computer and Communications Security (CCS 2025)
Edition / version
Methods
Software
Geographic location
Date collected
Date created
Subject
End-to-end verification; Network security; Secure routing; Verified systems
Organisational unit
03634 - Basin, David / Basin, David
03653 - Müller, Peter / Müller, Peter
03975 - Perrig, Adrian / Perrig, Adrian
02660 - Institut für Informationssicherheit / Institute of Information Security
02664 - Inst. f. Programmiersprachen u. -systeme / Inst. Programming Languages and Systems
Notes
Funding
87152 - NGI Pointer (EC)
Related publications and datasets
Is new version of: