VerifiedSCION

This package contains the verified implementation of the router from the SCION protocol, a future Internet architecture. SCION is the first clean-slate Internet architecture designed to provide route control, failure isolation, and explicit trust information for end-to-end communication.

To find out more about the project, please visit the official project page.

This repository contains a recent version of SCION (which we plan to keep updated), as well as fixes to the bugs we report as a result of verifying the SCION router from the mainline SCION repository.

Methodology

We focus on verifying the main implementation of SCION, written in the Go programming language.

To that end, we have developed Gobra, a program verifier for Go. Gobra allows users to annotate Go code with specifications in the form of logical assertions establishing the behaviour of the program. It then automatically checks whether the implementation matches its given specification. We use Gobra in the CI of this project via the gobra-action to verify our code-base.

In this project, we aim at verifying the data-plane component of the SCION border router. In particular, we verify the following properties:

1. memory safety, crash freedom, and race-freedom of the SCION data-plane code
2. progress properties and termination of the data-plane code
3. the IO behaviour of the router successfully refines the SCION protocol - we prove this property only the handling of packets of type SCION (i.e., we ignore BFD packages for now)

When necessary, we make reasonable assumptions and explicitly state them.

Differences to scionproto/scion

This repository is meant to be updated frequently, to keep track of the changes in the SCION implementation (scionproto/scion).

We try to have minimal differences from the original code and we expect to contribute these changes to the upstream when we believe that they improve the original code.

Repo Structure

This repository contains all the code from scionproto/scion. Its directory structure is the same as the SCION repository, except that it includes the verification directory, which contains useful definitions for specifying and verifying the border router:

verification
├── dependencies # spec of 3rd-party dependencies
└── utils
    ├── definitions # useful definitions
    └── slices # slice predicates and operations

To specify and verify the border router, we often add specifications in .go files directly. We also introduce .gobra files containing ghost-code and predicate definitions specific to a package.

License