Verifing SCION’s Implemention with Gobra​

Even though the SCION protocol has been proven to have strong security properties, its implementation can, in principle, still suffer from errors that invalidate core properties of the protocol. To ensure the correctness of SCION’s Go implementation, Peter Müller’s research group developed Gobra, a program verifier for Go. Gobra verifies specification compliance, memory safety, and crash freedom of the SCION implementation and ensures its trustworthiness.




 

Related Posts

GeoVITe PoC

GeoVITe is a user-friendly geodata data access service. Large-scale data is transmitted from WSL to ETH, which we were able to speed up downloads using

Bandwidth Allocation​

Anapaya Systems built a bandwidth allocation system into the SCI-ED network infrastructure. This system protects flows’ reserved bandwidth against other best-effort flows, providing bandwidth guarantees

Verified Secure Internet Forwarding

The research team of David Basin is verifying the correctness of SCION’s design and security protocols. The video below explains the mechanisms and approaches that

IT Lehrlabor

Exciting Opportunities for ETH’s IT Training Lab As part of the SCI-ED Project, we are aiming to expand the audience that will come in contact