Formal Development of Secure Data Plane Protocols

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 issues while simultaneously empowering end hosts. In these architectures autonomous systems authorize forwarding paths in accordance with their routing policies, and protect paths using cryptographic authenticators. For each packet, the sending end host selects an authorized paths and embeds it and its authenticators in the 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, that we call path authorization, protects the routing policies of autonomous from malicious senders. Further security properties are source authentication, which allows routers and the destination to authenticate the sender, and path validation, which allows the sender and the destination to verify that the packet traversed the path embedded in the header. Existing schemes that achieve these properties require long authenticators to be embedded in each packet's header. We propose EPIC, a family of protocols that achieve the same guarantees with substantially reduced overhead. The fundamental role of packet forwarding in the Internet's ecosystem and the complexity of the authentication mechanisms employed call for a formal analysis of EPIC, and of related protocols. We develop 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 that allow us to prove the refinement of the abstract model. We propose two novel attacker models and two sets of assumptions on the underlying routing protocol that allow us to classify protocols and distinguish them by how strong their guarantees are. We validate our framework by instantiating it with several concrete protocols and proving that they each satisfy the verification conditions (and hence path authorization). Invariants needed for the security proof are proven in the parametrized model; instances do not need to show invariants. Our framework thus supports low-effort security proofs for data plane protocols. We extend our framework in multiple ways, to allow a wide range of protocols and different attackers to be modeled. Our verification results hold for arbitrary network topologies and sets of authorized paths, a generality that state-of-the-art automated protocol verifiers cannot currently provide.