Co-authors: Peter Müller and David Basin
Despite the rapid advancements in technology, the uncomfortable truth is that most IT systems remain vulnerable to security attacks, with security breaches being an inevitable reality for many organizations. A major reason for this situation is that even small bugs - which seem difficult to avoid in complex IT systems - can be exploited by attackers, for instance, to gain unauthorized access or to disrupt availability.
The developers of SCION are using state-of-the-art practices for the design, development, and quality assurance to minimize any vulnerabilities in the system. Going even further, Anapaya and ETH Zurich have teamed up to take SCION’s security to a whole new level, by using mathematical proofs to eradicate entire classes of vulnerabilities. In this blog post, we give an overview of our approach and explain how it ensures that SCION delivers on its promise to provide secure connectivity.
In this blog post, we provide an overview of our approach and explain how it ensures that SCION delivers on its promise to provide secure network connectivity and a secure internet architecture.
Formal verification for SCION network security
Let’s take a closer look. Modern IT systems can execute in many different ways, depending on their inputs, the runtime environment (e.g., thread schedule), and their interactions with other systems, such as when receiving packets from other routers. In fact, a system generally has infinitely many possible executions, and having a bug in only one of them can make the system vulnerable if an attacker can exploit it. Hence testing, even when done extremely thoroughly, can cover only a tiny fraction of all possible executions and might miss bugs and vulnerabilities.
Let’s illustrate this problem with an analogy from mathematics. Imagine somebody claims that the sum of the first N natural numbers is equal to N(N+1)/2. You could apply testing to check whether this claim is true, by trying 3, 11, and 17 as values for N and observing that the claim holds in all three cases. That will certainly increase your confidence, but it is far from providing any assurance. Imagine the claim instead was “all odd numbers are prime”. The same three tests would succeed here as well, even though the claim is clearly false! Testing would provide absolute assurance only if we tried all possible inputs, but since there are infinitely many, that is not an option.
Fortunately, mathematics tells us how to make statements about infinitely many inputs: Instead of trying them one by one, we perform a mathematical proof that a claim holds for all possible inputs. For summing up the first N natural numbers, this is a simple induction proof; for the prime numbers, any proof attempt will fail, possibly providing us with a counterexample that clearly shows that the claim is false.
The same basic idea applies to software: we can treat programs as mathematical objects, formulate claims about their behavior, and use mathematical proofs to demonstrate that the claims are actually true. This process is called formal verification and that’s what we use to demonstrate that SCION is secure, definitely. Since IT systems are complex, proofs of their security may sometimes be long and tedious. To avoid human errors in the process, all our proofs are checked by software tools that ensure that we did not forget a case or draw a wrong conclusion. This tool support makes our results also less prone to human error than reviews or audits, which are useful, but cannot provide any guarantees.
SCION protocol verification
Our work so far has focused on SCION’s data plane, the part of SCION responsible for forwarding packets from the sender to the receiver. The control plane (for instance, SCION’s path discovery) is of course also important and will be tackled in future efforts.
SCION’s data plane protocol describes how packets are forwarded by each router on the path from the sender to the receiver. This protocol needs to ensure essential security properties, such as geofencing, even in the presence of attackers in the network. Since the protocol plays such an important role, verification starts there.
o prove properties of the SCION data plane protocol, we developed a mathematical model of an entire SCION network (illustrated by the upper half in the above diagram). This model includes the actors in such a network, such as routers and end hosts, and the connections between them. It also specifies exactly under which conditions a router forwards a packet, and to whom. In particular, the model includes mathematical formulations of all the checks prescribed by the SCION protocol, for instance, to ensure that a packet is forwarded only if the path stored in its header is valid.
Our overall goal is to prove that SCION is secure. For instance, an attacker cannot affect the path over which a packet travels unless it controls a router on that path. Whether such properties hold depends of course on the capabilities of the attacker. For instance, in the extremely unlikely case that an attacker could break SCION’s state-of-the-art cryptographic protection, it could manipulate and forge paths at will.
All statements about security, and especially all proofs of security properties, are always relative to an attacker’s capabilities. The specification of these capabilities is called an attacker model and is also included in our formal model of the SCION network. To obtain strong security guarantees, we prove that SCION is secure even in the presence of a very powerful attacker that may control several autonomous systems (such as ISPs), communicate also outside the SCION network, and observe, block, and inject packets.
Once we have a mathematical model of the SCION data plane, we can formalize its security properties. The most important of those is path authorization: a packet will travel only along previously-authorized paths (unless one of the autonomous systems on the path has been compromised). Path authorization provides senders with transparency and control over routing paths: It ensures senders that their packets will actually follow the path they choose. It also enables other important security properties, such as geofencing.
The actual proof shows that each possible step taken by an actor in the mathematical model, including the attacker, satisfies the specified security properties. We have carried out the proof in Isabelle/HOL (https://isabelle.in.tum.de/), a mature theorem-proving system that allows users to develop proofs interactively. The theorem prover checks that each proof step is valid and, thus, rules out mistakes. In the process, we found four subtle vulnerabilities in early versions of the SCION data plane protocol; all of which have long been fixed.
Code verification for next-generation networks
Having verified protocols is a huge step toward a trustworthy Internet. However, even if all protocol designs are secure, the actually deployed network could still be vulnerable if the software running on the network components, especially the routers, did not implement the protocol correctly.
For example, forgetting to perform a cryptographic check prescribed by the protocol, or performing it wrongly, could invalidate all security guarantees. To rule out errors in the concrete implementation, we formally verify the SCION implementation, in addition to the protocols. Like for the protocols, we started the code verification with the packet-forwarding functionality of the SCION data plane, by verifying the reference implementation of the SCION border router.
To verify the router implementation, we annotated the source code with specifications that express the intended properties, as well as with hints that allow a program verification tool to check automatically whether the program satisfies these properties. For this task, we developed our own program verification tool for the Go language, called Gobra. Gobra supports most of the Go language and can reason about a wide range of correctness and security properties. It verifies programs modularly, one method at a time, which is important to scale code verification to large implementations. The screenshot above shows how Gobra reports a verification error.
For the SCION router, we have verified four important properties. First, we proved that the router does not crash, for instance, due to an out-of-bounds access. Consequently, attackers cannot compromise the availability of the SCION network by causing its routers to crash. Second, we proved the various methods and data structures in the router are functionally correct, which is an important building block for other proofs. Third, we proved that packet forwarding makes progress. This rules out implementations that do nothing; such routers would be secure in a mathematical sense, but obviously of no practical use. Finally, we proved the most important aspect, namely that the router implements the SCION protocol correctly (see lower half of the diagram above). This step links the code verification to the formalization of the SCION protocol that we discussed above, making sure that all properties proved for the protocol's design actually hold also for the protocol’s implementation.
Conclusion
Overall, formal verification has proven very effective in making SCION even more secure. Our proofs have uncovered several implementation errors that could be fixed early in the development pipeline. We will soon publish a paper with a detailed analysis on our findings.
Nevertheless, even tool-checked mathematical proofs have limitations, which affect the provided guarantees. Our verification effort covers the SCION data plane protocol and its implementation in the SCION router. Even if those components are secure, it might be possible to attack other parts of a deployed network, for instance, the operating system and hardware on which routers run. Hence, we still need to rely on best practices to harden those components; nevertheless, verification has drastically reduced the overall attack surface.
In summary, SCION’s verification provides unprecedented security guarantees for both protocols and code, and demonstrates that SCION indeed lives up to its promise. The formalization of the SCION protocols and their properties additionally provide a thorough description that will also facilitate the ongoing standardization effort.
The verification of SCION is a work in progress: Anapaya and ETH Zurich have just obtained funding from NGI to speed up the project. Our next goals include verifying the control plane, extending code verification to components and libraries previously omitted, and developing ways to maintain the code-level proofs as the router evolves. If you are interested in learning more, stay tuned for subsequent blog posts and check out Part VI of the SCION book!
