IsaNet: A framework for verifying secure data plane protocols

Article type: Research Article

Authors: Klenze, Tobias | Sprenger, Christoph^{; *} | Basin, David

Affiliations: Department of Computer Science, ETH Zurich, Switzerland

Correspondence: [*] Corresponding author. E-mail: [email protected].

Abstract: Today’s Internet is built on decades-old networking protocols that lack scalability, reliability and security. In response, the networking community has developed path-aware Internet architectures that solve these problems while simultaneously empowering end hosts to exert some control on their packets’ route through the network. In these architectures, autonomous systems authorize forwarding paths in accordance with their routing policies, and protect these paths using cryptographic authenticators. For each packet, the sending end host selects an authorized path and embeds it and its authenticators in the packet header. This allows routers to efficiently determine how to forward the packet. The central security property of the data plane, i.e., of forwarding, is that packets can only travel along authorized paths. This property, which we call path authorization, protects the routing policies of autonomous systems from malicious senders. The fundamental role of packet forwarding in the Internet’s ecosystem and the complexity of the authentication mechanisms employed call for a formal analysis. We develop IsaNet, a parameterized verification framework for data plane protocols in Isabelle/HOL. We first formulate an abstract model without an attacker for which we prove path authorization. We then refine this model by introducing a Dolev–Yao attacker and by protecting authorized paths using (generic) cryptographic validation fields. This model is parametrized by the path authorization mechanism and assumes five simple verification conditions. We propose novel attacker models and different sets of assumptions on the underlying routing protocol. We validate our framework by instantiating it with nine concrete protocol variants and prove that they each satisfy the verification conditions (and hence path authorization). The invariants needed for the security proof are proven in the parametrized model instead of the instance models. Our framework thus supports low-effort security proofs for data plane protocols. In contrast to what could be achieved with state-of-the-art automated protocol verifiers, our results hold for arbitrary network topologies and sets of authorized paths.

Keywords: Security protocols, formal verification, future Internet, data plane

DOI: 10.3233/JCS-220021

Journal: Journal of Computer Security, vol. 31, no. 3, pp. 217-259, 2023