VerifiedSCION
The goal of this project is to verify the SCION Next-Generation Internet architecture, all the way from high-level protocols to executable code.
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 external page 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.
Links
Watch a short Download video (MP4, 31.7 MB) about our project
Listen to an interview in this external page Podcast
Project Members
João Carlos Mendes Pereira
Peter Müller
Dionisios Spiliopoulos
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 designing techniques for proving security properties of object-oriented programs and developing automatic verifiers for Go and Python code with static type annotations, based on the Viper verification infrastructure.
Publications
- J. C. Pereira, T. Klenze, S. Giampietro, M. Limbeck, D. Spiliopoulos, F. A. Wolf, M. Eilers, C. Sprenger, D. Basin, P. Müller, and A. Perrig: Protocols to Code: Formal Verification of a Next-Generation Internet Router
Technical Report, 2024. [PDF] [BIB] [external page arXiv]
- F. A. Wolf and L. Arquint and M. Clochard and W. Oortwijn and J. C. Pereira and P. Müller: Gobra: Modular Specification and Verification of Go Programs
In Computer Aided Verification (CAV), 2021. [Download PDF][BIB][external page Talk]
- C. Sprenger, T. Klenze, M. Eilers, F. A. Wolf, P. Müller, M. Clochard, and D. Basin: Igloo: Soundly Linking Compositional Refinement and Separation Logic for Distributed System Verification
In Object-Oriented Programming Systems, Languages, and Applications (OOPSLA), 2020. [Download PDF][BIB][external page Talk] - M. Eilers and P. Müller, Nagini: A Static Verifier for Python
In Computer Aided Verification (CAV), 2018. [Download PDF][BIB]
- M. Eilers and P. Müller and S. Hitz, Modular Product Programs
In European Symposium on Programming (ESOP), 2018. [Download PDF][BIB]
Completed Student Projects
- Lino Telschow, Master's Thesis
Specifying and Verifying the IO Behavior of the SCION Border Router
- Severin Meier, Master's Thesis
Verification of Information Flow Security for Python Programs - Sascha Forster, Bachelor's Thesis
Static Verification of the SCION Router Implementation - Christian Knabenhans, Bachelor's Thesis
Automatic Inference of Hyperproperties - Vytautas Astrauskas, Master's Thesis
Input/Output Verification in Viper
Acknowledgments
The verifedSCION project has been partly funded by external page NGI0 Core and NGI Pointer.