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

arXiv:2405.06074v1 Announce Type: new
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, …

adversarial architecture arxiv code cryptographic cs.cr cs.ni cs.pl environment forwarding implementation internet low network next packet precisely protocol protocols router routers run security verification verified verify