Full-Stack Verification of Secure Inter-Domain Routing Protocols

Status

This project started on the 1st of September 2015 and is ongoing.

Researchers

Information Security – ETH

Prof. David Basin
Dr. Christoph Sprenger
Dr. Ralf Sasse
Tobias Klenze
Dr. Si Liu
Shabnam Ghasemirad

Programming Methodology – ETH

Prof. Peter Müller
Marco Eilers
Wytse Oortwijn
Dr. Martin Clochard
Linard Arquint
João Carlos Mendes Pereira
Felix Wolf

Network Security – ETH

Prof. Adrian Perrig
Dr. Markus Legner
Joel Wanner

Former Project Members

Fábio Pakk Selmi-Dei
Wytse Oortwijn
Samuel Hitz

Description

Inter-domain routing is a part of the Internet’s core infrastructure. The currently used Border Gateway Protocol suffers from attacks leading to severe disruptions of the Internet. This prompted the development of the secure Internet architecture SCION. In this research project, we examine the SCION protocols in detail and formally verify that they have the desired security properties. We first formalize the protocols and security guarantees, and then use techniques from refinement and interactive theorem proving for their verification. Finally, we extract from the proven assertions a low-level specification of the IO-behavior of SCION components.

We then use this specification to formally verify the Go implementation of the SCION router. In particular, we prove the absence of runtime errors and the implementation’s compliance with the specification, i.e., its functional correctness. Additionally, we prove security-related properties of the implementation like secure information flow.

Since the verification effort on the protocol level uses a different formalism than the verification of the code level, a sound link has to be created between them. We realize this link by a refinement step that translates the abstract model into a specification of its IO-behavior. The soundness of this translation is proved in an interactive theorem prover.

Our goal is to gain a better understanding of the underlying properties of the SCION protocol and routing protocols in general, and to improve on the state of the art for the verification of concurrent, object-oriented programs. Moreover, this work will contribute to the first Internet protocol suite that has been verified from the ground up.

In 2020 we published our “Igloo” framework, which realizes the sound link between protocol and code and provides the methodology for full-stack verification. We have also made substantial steps in the modelling of the SCION forwarding protocol and the tools required to verify its implementations.

Progress

We have made substantial progress towards our goal of a full-stack verification of SCION routers, in particular the areas of protocol verification, code verification, and a sound link between these efforts. In 2020 we published our “Igloo” (OOPSLA’20) framework, which realizes the sound link between protocol and code and provides the methodology for full-stack verification.

In 2021 we successfully verified the SCION data plane protocol, as well as other protocols, in a parameterized verification framework. Our CSF’21 paper describes this framework. The most recent additions to this work, which allowed us to verify the current version of the SCION protocol, are not published yet.

We have also made substantial steps in the tools required to verify the SCION router implementation. In early 2021, we have completed a full-fledged Go verifier capable of handling Go’s advanced language features, namely channel-based concurrency and interfaces. A corresponding publication is in progress. Using our developed verifier, we are now in the process of proving that the data plane implementation of Scion’s border router satisfies memory safety, crash safety, and data race freedom.

Talks

David Basin, “Verified Secure Routing”, EPFL Summer Researcher Institute (SuRI), Lausanne Switzerland, June 2017.

Christoph Sprenger, “The verification of a secure internet architecture”, Formal Reasoning in Distributed Algorithms (FRIDA 2017), Satellite workshop of DISC 2017, Vienna, Austria, October 2017.

David Basin, “Verified Secure Routing”, 22th International Conference on Engineering of Complex Computer Systems (ICECCS), Fukuoka Japan, November 2017.

Peter Müller, “Verified Secure Routing”, Max-Planck Institute for Software Systems, Kaiserslautern, Germany, November 19, 2018. Distinguished Lecture.

Publications

Felix A. Wolf, Linard Arquint, Martin Clochard, Wytse Oortwijn, João C. Pereira, and Peter Müller
Gobra: Modular Specification and Verification of Go Programs
Computer Aided Verification (CAV), 2021.
PDF

Tobias Klenze, Christoph Sprenger, and David Basin.
Formal Verification of Secure Forwarding Protocols
Computer Security Foundations Symposium (CSF), 2021.
PDF

Christoph Sprenger, Tobias Klenze, Marco Eilers, Felix A. Wolf, Peter Müller, Martin Clochard, and David Basin
Igloo: Soundly Linking Compositional Refinement and Separation Logic for Distributed System Verification
OOPSLA 2020.
PDF

Marco Eilers, Peter Müller, and Samuel Hitz
Modular product programs
TOPLAS 2019
PDF

Marco Eilers and Peter Müller and Samuel Hitz
Modular Product Programs
European Symposium on Programming (ESOP), 2018.
PDF

Marco Eilers and Peter Müller
Nagini: A Static Verifier for Python
Computer Aided Verification (CAV), 2018.
PDF