VerifiedSCION
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 pageSCION (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 Downloadvideo (MP4, 31.7 MB) about our project
Listen to an interview in this external pagePodcast
Project Members
João Carlos Mendes Pereira
Peter Müller
Dionisios Spiliopoulos
Felix Wolf
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
- 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. [DownloadPDF][BIB][external pageTalk]
- 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. [DownloadPDF][BIB][external pageTalk] - M. Eilers and P. Müller, Nagini: A Static Verifier for Python
In Computer Aided Verification (CAV), 2018. [DownloadPDF][BIB]
- M. Eilers and P. Müller and S. Hitz, Modular Product Programs
In European Symposium on Programming (ESOP), 2018. [DownloadPDF][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 NGI Pointer.