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.

翻译：我们提出了首个经过形式化验证的互联网路由器，该路由器是SCION互联网架构的组成部分。SCION路由器运行加密协议，在对抗性环境中实现安全的数据包转发。我们不仅验证了该协议的网络级安全属性，还验证了其实现的底层属性。具体而言，我们通过Isabelle/HOL中的精化方法开发了一系列协议模型，并使用自动化程序验证工具证明该路由器的Go代码满足内存安全、无崩溃、无数据竞争，并遵循协议模型。这两项验证工作被牢固地关联在一起。我们的工作证明了从高层协议模型到由独立团队开发的性能优化生产代码，对关键网络组件进行一致验证的可行性。在此过程中，我们发现了协议及其实现中的关键漏洞（已得到代码开发者确认），并增强了协议的安全属性。本文阐述了我们的方法，总结了主要成果，并提炼了关于可验证系统的设计与实现、持续变更的处理策略以及所采用的验证技术与工具方面的经验教训。