Skip to main content
Top

2022 | Book

The Complete Guide to SCION

From Design Principles to Formal Verification

Authors: Dr. Laurent Chuat, Dr. Markus Legner, Prof. Dr. David Basin, Prof. Dr. David Hausheer, Samuel Hitz, Prof. Dr. Peter Müller, Prof. Dr. Adrian Perrig

Publisher: Springer International Publishing

Book Series : Information Security and Cryptography

insite
SEARCH

About this book

When the SCION project started in 2009, the goal was to create an architecture offering high availability and security for basic point-to-point communication. In the five years since the publication of SCION: A Secure Internet Architecture, this next-generation Internet architecture has evolved in terms of both design and deployment.

On the one hand, there has been development of exciting new concepts and systems, including a new global time-synchronization system, an inter-domain approach for bandwidth reservations called COLIBRI, and Green Networking, which allows combating global climate change on three fronts. On the other hand, SCION is now also in production use by the Swiss financial ecosystem, and enables participants such as the Swiss National Bank, the Swiss provider of clearing services (SIX), and all Swiss financial institutes to communicate securely and reliably with each other via the Secure Swiss Finance Network.

This unique guidebook provides an updated description of SCION's main components, covering new research topics and the most recent deployments. In particular, it presents in-depth discussion of formal verification efforts. Importantly, it offers a comprehensive, thorough description of the current SCION system:

Describes the principles that guided SCION's design as a secure and robust Internet architecture

Provides a comprehensive description of the next evolution in the way data finds its way through the Internet

Explains how SCION can contribute to reducing carbon emissions, by introducing SCION Green Networking

Demonstrates how SCION not only functions in academic settings but also works in production deployments

Discusses additional use cases for driving SCION's adoption

Presents the approaches for formal verification of protocols and code

Illustrated with many colorful figures, pictures, and diagrams, allowing easy access to the concepts and use cases

Assembled by a team with extensive experience in the fields of computer networks and security, this text/reference is suitable for researchers, practitioners, and graduate students interested in network security. Also, readers with limited background in computer networking but with a desire to know more about SCION will benefit from an overview of relevant chapters in the beginning of the book.

Table of Contents

Frontmatter
Chapter 1. Introduction
Abstract
The Internet has been successful beyond even the most optimistic expectations. It permeates and is intertwined with many aspects of our society. This success has created a fundamental dependency on communication, as many of the processes underpinning modern society would grind to a halt should the Internet become unavailable. Unfortunately, the security of today’s Internet is far from commensurate with its importance as critical infrastructure.
Laurent Chuat, Markus Legner, David Basin, David Hausheer, Samuel Hitz, Peter Müller, Adrian Perrig

SCION Core Components

Frontmatter
Chapter 2. Overview
Abstract
To briefly reiterate the vision we presented in the first chapter, our main goal is to design a network architecture that offers highly available and efficient point-to-point packet delivery—even in the presence of actively malicious entities. SCION introduces the concept of isolation domains (ISDs)*ISD constitutes a logical grouping of autonomous systems (ASes), as depicted in Figure 2.1. Each ISD is administered by a few distinguished ASes that we refer to as core ASes*, and usually also contains multiple non-core ASes. An AS can join an ISD by connecting to another AS in the ISD.
Laurent Chuat, Markus Legner, David Basin, David Hausheer, Samuel Hitz, Peter Müller, Adrian Perrig
Chapter 3. Authentication
Abstract
In contrast to the legacy Internet, SCION was designed and built with security as one of the primary objectives. Therefore, all control-plane messages are authenticated. The verification of those messages relies on a public-key infrastructure (PKI) called the control-plane PKI or CP-PKI. In short, the CPPKI is a set of mechanisms, roles, and policies related to the management and usage of certificates, which enable the verification of signatures, e.g., on path segment construction beacons (PCBs).
Laurent Chuat, Markus Legner, David Basin, David Hausheer, Samuel Hitz, Peter Müller, Adrian Perrig
Chapter 4. Control Plane
Abstract
This chapter describes SCION's control plane, whose main purpose is to create and manage path segments, which can then be combined into forwarding paths to transmit packets in the data plane. We first discuss how path exploration is realized through beaconing and how path segments are registered. We then discuss path lookup and present the SCION Control Message Protocol (SCMP).
Laurent Chuat, Markus Legner, David Basin, David Hausheer, Samuel Hitz, Peter Müller, Adrian Perrig
Chapter 5. Data Plane
Abstract
The ultimate purpose of any network is to deliver data between end hosts,which is the responsibility of the data plane. SCION's data plane is fundamentally different from today's IP-based data plane in that it is path-aware: In SCION, inter-domain forwarding directives are embedded in the packet header as a sequence of hop fields (HFs), which encode AS-level hops augmented with ingress and egress interface identifiers.
Laurent Chuat, Markus Legner, David Basin, David Hausheer, Samuel Hitz, Peter Müller, Adrian Perrig

Analysis of the Core Components

Frontmatter
Chapter 6. Functional Properties and Scalability
Abstract
In Chaps. 2–5, we have presented the main components of the SCION architecture: beacon service, certificate service, and path service; the concept of ISDs and their trust root configuration (TRC); the CP-PKI and symmetrickey infrastructure; the path-exploration (beaconing), -registration, and -lookup mechanisms; and the SCION forwarding process.
Laurent Chuat, Markus Legner, David Basin, David Hausheer, Samuel Hitz, Peter Müller, Adrian Perrig
Chapter 7. Security Analysis
Abstract
One of the fundamental objectives that guided the design of SCION is security, in particular network security.
Laurent Chuat, Markus Legner, David Basin, David Hausheer, Samuel Hitz, Peter Müller, Adrian Perrig

Achieving Global Availability Guarantees

Frontmatter
Chapter 8. Extensions for the Control Plane
Abstract
SCION’s extensible architecture enables new systems that can take advantage of the novel properties and mechanisms provided. As compared to the current Internet, most of the benefits are achieved through the use of packet-carried forwarding state (PCFS), path transparency, and control. In this chapter, we describe three control-plane systems to supplement the SCION architecture: Hidden paths enable the selective announcement of path segment information to chosen recipients; the SCION time synchronization provides highly secure, available, and scalable global time; and finally, we highlight the power of adding metadata about paths to PCBs.
Laurent Chuat, Markus Legner, David Basin, David Hausheer, Samuel Hitz, Peter Müller, Adrian Perrig
Chapter 9. Monitoring and Filtering
Abstract
An important aspect of achieving security for SCION is not only to ensure correct operations by preventing malicious activities, but also to detect misbehavior. For instance, a MAC or digital signature prevents adversaries from forging or altering authenticated information. However, an adversary may still duplicate legitimate packets to perform a DoS attack by overflowing links (§9.1), sending excessive numbers of packets to overwhelm end systems (§9.2), or simply sending too much traffic, thus causing congestion in the network (§9.3). This chapter presents SCION’s countermeasures, which all can be implemented efficiently on high-speed routers and end systems.
Laurent Chuat, Markus Legner, David Basin, David Hausheer, Samuel Hitz, Peter Müller, Adrian Perrig
Chapter 10. Extensions for the Data Plane
Abstract
Two of the most surprising properties SCION enables are that—for the first time—minimum bandwidth guarantees and highly efficient per-packet source authentication can be achieved on global communication networks. Such properties were so far considered elusive at best, and impossible at worst. In this chapter, we describe the technical innovations and systems that lead to the accomplishment of these two properties, while the following chapter discusses how the interaction between all elements within the entire SCION ecosystem, including the here-mentioned innovations, ensures the availability and authenticity of communications end-to-end.
Laurent Chuat, Markus Legner, David Basin, David Hausheer, Samuel Hitz, Peter Müller, Adrian Perrig
Chapter 11. Availability Guarantees
Abstract
As we argue in Chapter 7, the most fundamental requirement for any networking architecture is to be available: It is trivial to design a perfectly secure but unavailable network by simply cutting all connections or dropping all packets. Unfortunately, the current Internet falls short of achieving availability in an adversarial environment despite a multitude of defense mechanisms; in contrast, availability was a core requirement during the design of the SCION architecture.
Laurent Chuat, Markus Legner, David Basin, David Hausheer, Samuel Hitz, Peter Müller, Adrian Perrig

SCION in the Real World

Frontmatter
Chapter 12. Host Structure
Abstract
In this chapter, we discuss how SCION-enabled end hosts can benefit from SCION properties.
Laurent Chuat, Markus Legner, David Basin, David Hausheer, Samuel Hitz, Peter Müller, Adrian Perrig
Chapter 13. Deployment and Operation
Abstract
This chapter presents deployment alternatives and network-operation approaches of the SCION Internet architecture.
Laurent Chuat, Markus Legner, David Basin, David Hausheer, Samuel Hitz, Peter Müller, Adrian Perrig
Chapter 14. SCIONLAB Research Testbed
Abstract
Throughout this book, we have seen how path-aware network architectures enable the creation of new applications and services, as they provide users with advanced communication features such as multipath, efficient key distribution, or geofencing.
Laurent Chuat, Markus Legner, David Basin, David Hausheer, Samuel Hitz, Peter Müller, Adrian Perrig
Chapter 15. Use Cases and Applications
Abstract
Numerous events have made the inadequacies of today’s Internet increasingly apparent. As SCION is able to achieve desirable properties for stakeholders in a wide variety of use cases, there exist many reasons to adopt SCION1 to overcome those limitations. In this chapter, we highlight some of the most promising use cases and applications that can benefit from SCION. Additionally, we also provide insights into concrete case studies where SCION has been applied successfully.
Laurent Chuat, Markus Legner, David Basin, David Hausheer, Samuel Hitz, Peter Müller, Adrian Perrig
Chapter 16. Green Networking with SCION
Abstract
Networking infrastructure (excluding data centers) is responsible for 270 TWh/yr or 1.1% of worldwide electricity consumption (in 2020) [28], which is expected to experience a ten-fold increase by 2030 due to the steady growth of Internet traffic volume [28, 29]. As electricity production emits considerable amounts of greenhouse gasses (475 gCO2/kWh [258]), Internet
Laurent Chuat, Markus Legner, David Basin, David Hausheer, Samuel Hitz, Peter Müller, Adrian Perrig
Chapter 17. Cryptography
Abstract
With security as a central objective, SCION naturally makes extensive use of cryptography. Different SCION components require different types of crypto-graphic primitives: symmetric and asymmetric. For example, while the control plane mainly relies on asymmetric cryptography in the form of signatures to enable any entity to verify the authenticity of the signed data and achieve non-repudiation, only symmetric primitives such as message authentication codes (MACs) are sufficiently efficient for data-plane packet processing.
Markus Legner, Adrian Perrig, Marc Wyss

Additional Security Systems

Frontmatter
Chapter 18. F-PKI: A Flexible End-Entity Public-Key Infrastructure
Abstract
In contrast to the control-plane PKI (presented in §3.1), whose main purpose is to authenticate ASes, an end-entity PKI enables the authentication of end systems such as web servers. It also facilitates the design of RHINE, a next-generation secure and reliable Internet naming system (Chapter 19). The most widely used end-entity PKI is the HTTPS public-key infrastructure (or Web PKI, for short). Unfortunately, today’s Web PKI suffers from a weakest-link problem: Any certification authority (CA) can issue certificates for any domain at will, and several events in the past few years have proven that this constitutes a real threat.
Laurent Chuat, Markus Legner, David Basin, David Hausheer, Samuel Hitz, Peter Müller, Adrian Perrig
Chapter 19. RHINE: Secure and Reliable Internet Naming Service
Abstract
Translating human-readable names to network addresses (among other information), a naming service is indispensable in making digital communication practically usable. Almost every connection over the Internet starts with a name resolution query to the Domain Name System (DNS). Likewise, for the setup of SCION connections, proper name resolution should precede path lookup: Before an endpoint can ask for paths to another endpoint, it must obtain a SCION address corresponding to the destination name.
Laurent Chuat, Markus Legner, David Basin, David Hausheer, Samuel Hitz, Peter Müller, Adrian Perrig
Chapter 20. PILA: Pervasive Internet-Wide Low-Latency Authentication
Abstract
PILA provides end-to-end encryption and authentication, increasing the minimum level of security of all communication.
Laurent Chuat, Markus Legner, David Basin, David Hausheer, Samuel Hitz, Peter Müller, Adrian Perrig

Formal Verification

Frontmatter
Chapter 21. Motivation for Formal Verification
Abstract
The construction of distributed systems is extremely challenging—especially for systems that operate in adversarial environments. SCION is no exception. A SCION network consists of a variety of different components such as routers, beacon servers, path servers, and edge devices.
Laurent Chuat, Markus Legner, David Basin, David Hausheer, Samuel Hitz, Peter Müller, Adrian Perrig
Chapter 22. Design-Level Verification
Abstract
In this chapter we present our verification of SCION at the protocol level. We describe two projects that are completed: the verification of SCION’s data describe two projects that are completed: the verification of SCION’s data.
Laurent Chuat, Markus Legner, David Basin, David Hausheer, Samuel Hitz, Peter Müller, Adrian Perrig
Chapter 23. Code-Level Verification
Abstract
The verification effort described so far ensures that the SCION protocol guarantees the intended correctness and security properties. These design-level guarantees are essential, but by themselves do not guarantee that a SCION network actually works as intended. Errors in the protocol’s implementation could compromise its availability, correctness, or security—for instance, by causing a component to crash, skip essential checks, or leak confidential information. To guarantee the absence of errors in the SCION implementation, we employ code-level verification. Design-level and code-level verification complement each other and target different abstractions of the overall system. In particular, design-level verification provides specifications for many of the properties that need to hold for the implementation to be correct, for instance, the intended I/O behavior of each component. Other properties, such as memory safety, data-race freedom, and the absence of backdoors are specified directly on the code level.
Laurent Chuat, Markus Legner, David Basin, David Hausheer, Samuel Hitz, Peter Müller, Adrian Perrig
Chapter 24. Current Status and Plans
Abstract
In the previous chapters we have motivated the need for formal methods—both at the design level and the code level—and discussed techniques for both levels. We have seen the results of verification efforts related to the SCION data plane and the N-Tube algorithm and discussed example code from the SCION border router.
Laurent Chuat, Markus Legner, David Basin, David Hausheer, Samuel Hitz, Peter Müller, Adrian Perrig

Back Matter

Frontmatter
Chapter 25. Related Work
Abstract
Given the extensive list of topics covered in this book, a wealth of related work exists. Balancing relevance, completeness and readability, we focus on related work specifically in the areas of future Internet architectures, deployment of new Internet architectures, and inter-domain multipath routing protocols. Current efforts to secure the current Internet inter-domain infrastructure are discussed in Section 1.1.3. For a more detailed treatment of related work pertaining to the various chapters of the book, we refer to the scientific papers of the respective topics, which all include a detailed discussion of related work.
Laurent Chuat, Markus Legner, David Basin, David Hausheer, Samuel Hitz, Peter Müller, Adrian Perrig
Backmatter
Metadata
Title
The Complete Guide to SCION
Authors
Dr. Laurent Chuat
Dr. Markus Legner
Prof. Dr. David Basin
Prof. Dr. David Hausheer
Samuel Hitz
Prof. Dr. Peter Müller
Prof. Dr. Adrian Perrig
Copyright Year
2022
Electronic ISBN
978-3-031-05288-0
Print ISBN
978-3-031-05287-3
DOI
https://doi.org/10.1007/978-3-031-05288-0

Premium Partner