Inter-domain routing is a part of the internet's core infrastructure. Despite its important role, the currently most widely deployed Border Gateway Protocol (BGP) has been observed to suffer from attacks, leading to severe disruptions of the Internet. This prompted the development of SCION (Scalability, Control and Isolation on Next-Generation Networks). SCION is a clean-slate Internet architecture that provides secure routing and forwarding, alongside a number of other desirable properties.
This research project is a joint effort with the Network Security Group and the Information Security Group. Its goal it is to verify the routing protocol SCION from the high-level design all the way down to the implementation. The focus of our group is on verifying safety, functional correctness, and security of the implementation of the SCION routers. For this purpose, we are currently building an automatic verifier for Python code with static type annotations based on the Viper verification infrastructure.