Protocols to Code: Formal Verification of a Next-Generation Internet Router
arxiv(2024)
摘要
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.
更多查看译文
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要