Toward a Fully-Verified SCION Router

SCION is a next-generation Internet architecture that addresses many of the security vulnerabilities of today’s Internet. Its clean-slate design provides, among other properties, route control, failure isolation, and multi-path communication. This project will demonstrate the feasibility of verifying the core component of the SCION inter-domain routing architecture - the SCION router. Prior work has proved that the SCION data plane protocols are secure. The focus of this project is on verifying that SCION’s open-source router is memory-safe and implements those protocols correctly and, thus, provides the intended security and correctness guarantees.