Code-Level Verification
METADATA ONLY
Loading...
Author / Producer
Date
2022
Publication Type
Book Chapter
ETH Bibliography
yes
Citations
Altmetric
METADATA ONLY
Data
Rights / License
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.
Permanent link
Publication status
published
Book title
The Complete Guide to SCION: From Design Principles to Formal Verification
Journal / series
Volume
Pages / Article No.
519 - 562
Publisher
Springer
Event
Edition / version
Methods
Software
Geographic location
Date collected
Date created
Subject
Organisational unit
03653 - Müller, Peter / Müller, Peter
Notes
Funding
Related publications and datasets
Is part of: