Full-Stack Verification of Secure Inter-Domain Routing Protocols

Status

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

Researchers

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 a secure Internet architecture, SCION. In this research project, we examine the SCION protocols in detail and formally verify their desired functional and security properties. We do this both at the modeling and the implementation level. Our goal is to gain a better understanding of the underlying properties of the SCION protocols and routing protocols in general, and to improve on the state of the art for the verification of concurrent programs.

A milestone in this project was successfully completing the full-stack verification of the SCION data plane protocols. To the best of our knowledge, the SCION router is now the first deployed networking infrastructure component to have been comprehensively verified for both network-wide security properties and local code properties.

To achieve this, we used the combined model-and-code verification technique that we previously developed. We first formalized the data plane protocols and their security properties (e.g. network-wide properties such as path authorization or loop freedom). We then used refinement to derive more concrete protocol models from which we automatically extracted program specifications expressing the implementation’s desired I/O behavior (called I/O specifications). All these steps were formalized in the interactive theorem prover Isabelle/HOL. In particular, we have proved the correctness of all the refinement steps as well as the soundness of the translation from protocol models to I/O specifications.

We then used Gobra, a code verifier, to prove the functional correctness of the implementation: namely we verified that the router code satisfies memory and crash safety, race freedom, and that it adheres to the I/O specification generated from the protocol models. This required new verification techniques for the language features and software designs used by the router’s Go code, and substantial performance improvements to Gobra to handle the code’s complexity.

As both verification efforts are soundly linked together, our verification effort guarantees that the security properties proved for the protocol also hold for the executing system. The paper presenting this work is currently under submission [https://arxiv.org/abs/2405.06074].

Building upon our success with the data plane verification, the next step in this project is the verification of the SCION control plane. The control plane protocols are specified in an IETF draft standard that defines packet formats and high-level goals, while the detailed protocol behaviors are currently documented through an open source reference implementation.

So far, we have developed a formal model of the control plane that provides a complete and precise specification of protocol behaviors. This model serves multiple purposes: it provides an implementation-independent description of the protocols, enables formal reasoning about protocol properties, and can serve as a clear reference for developing new implementations. We have also formalized the desired security properties, creating precise definitions that can be used in formal verification. We are currently working on aligning our formal model and the IETF standard.

Our ongoing work focuses on formally verifying that the control plane satisfies the desired security properties at the design level. Notably, our previous data plane verification relies on assumptions about the correctness of the control plane, making this verification effort essential to establish the practical security guarantees of the entire system and moving us closer to a comprehensively verified secure Internet architecture.

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

João C. Pereira, Tobias Klenze, Sofia Giampietro, Markus Limbeck, Dionysios Spiliopoulos, Felix A. Wolf, Marco Eilers, Christoph Sprenger, David Basin, Peter Müller, Adrian Perrig
Protocols to Code: Formal Verification of a Next-Generation Internet Router
arXiv 2024.

Linard Arquint, Felix A. Wolf, Joseph Lallemand, Ralf Sasse, Christoph Sprenger, Sven N. Wiesener, David Basin, and Peter Müller
Sound Verification of Security Protocols: From Design to Interoperable Implementations
IEEE Symposium on Security and Privacy, SP 2023.
PDF

Tobias Klenze, Christoph Sprenger, and David Basin
IsaNet: A Framework for Verifying Secure Data Plane Protocols
Journal of Computer Security, 2022.
PDF

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