Sam Hitz and Peter Müller are testing the architecture that underpins the Internet for secure routing using maths and tool-checked proofs.
What’s SCION and why the need for VerifiedSCION?
SCION – Scalability, Control and Isolation on Next-Generation Networks – is a clean-slate Internet architecture that provides secure routing and forwarding, alongside a number of other desirable properties. It combines performance and reliability with strong security properties. Such as the guarantee that packets will travel only along previously-authorized paths, eradicating the traffic-attraction attacks of today’s Internet and enabling sophisticated traffic control such as geofencing.
The goal of our project, VerifiedSCION is to provide strong evidence for SCION’s security properties – mathematical, tool-checked proofs that verify SCION’s security from high-level specifications all the way to the code executing on a router.
Introduce your team – and your motivation to work on VerifiedSCION
The most widely deployed inter-domain routing on the Internet, Border Gateway Protocol (BGP) has been observed to suffer from attacks, leading to severe disruptions. An ambitious project such as verifying the SCION Internet architecture requires a diverse set of skills. We assembled a team of network networking, security, and verification experts. Adrian Perrig and his group at ETH Zurich and Sam Hitz at Anapaya Systems, a start-up company that commercialises the SCION architecture, bring in the domain and design expertise. David Basin and his group at ETH Zurich have substantial experience in information security and, in particular, the verification of security protocols. Finally, Peter Müller and his team at ETH Zurich contribute their experience in code-level verification.
All team members are motivated by the same vision: providing the world with fast, reliable and secure communication. We are convinced that SCION has the potential to disrupt the Internet, and that verification is an essential element in providing a Next Generation Internet that individuals and companies can fully trust.
What does it mean to formally verify an Internet architecture?
Formal verification proves that an artifact such as a communication protocol or a software implementation satisfies a precise specification of its intended behaviour. Such specifications can range from basic properties like “the program will not crash” to sophisticated correctness and security properties. A key virtue of verification is that, unlike testing, a proof covers all possible ways of executing a program – for all inputs, all thread schedules, and all possible interactions with the environment.
An essential part of verifying the SCION Internet architecture is to prove that the SCION routing protocol is correct. To this end, we distil and formalize the security requirements SCION has to satisfy. Moreover, we develop formal models of the SCION protocol as well as an attacker model, which describes the ways in which an attacker can interfere with the communication, for instance, by intercepting or forging messages. The central result is a formal proof, checked by a tool, that the SCION protocol satisfies all the specified properties, even in the presence of a powerful attacker.
Establishing formal guarantees for the SCION protocol is a milestone for Internet security. However, our goal is to go much further: We are using program verification techniques to prove that the actual implementation that runs on each SCION router implements the protocol correctly, does not crash, and does not include backdoors that could allow attackers to obtain cryptographic keys and other confidential information. With this code-level verification, we establish, for the first time, formal end-to-end security guarantees for an Internet protocol, linking high-level specifications all the way down to executable code.
What makes it possible to verify a whole Internet architecture?
One crucial success factor for our project is the development of suitable verification techniques and tools. In particular, prior to this NGI project, we built a program verification tool for the Go programming language that supports all language features and properties required for the SCION verification. Moreover, we developed a novel technique to formally link protocol-level proofs and code-level proofs, which enables us to provide end-to-end guarantees.
A possibly even more critical success factor is that SCION has been designed with verifiability in mind. The SCION protocol requires routers that are orders of magnitude simpler than BGP routers. As a result, the code running on a SCION router is sufficiently small and simple to make verification possible.
What’s the difference NGI made to your project?
The NGI Pointer support provided an excellent opportunity to bring together a team from different institutions to undertake this ambitious project and to demonstrate that it is now possible to develop a Next Generation Internet architecture that is provably secure. We are also eager to demonstrate that the verification techniques and tools that we have developed are sufficiently powerful to take on a project of this size and ambition.
Our project is well on track and has not been substantially affected by the pandemic. If anything, our many video conferences have further increased our desire to provide the world with fast and reliable communication.
More information
VerifiedSCION project: https://www.pm.inf.ethz.ch/research/verifiedscion/NGI.html
SCION: https://www.scion-architecture.net/
Footprints on the path: how routing data could reduce the internet’s carbon toll: https://www.weforum.org/agenda/2021/03/internet-carbon-emissions-data-path-scion/