Header space analysis: static checking for networks

TLDR

Modern networks deploy many protocols (MPLS, NAT, ACLs, route redistribution) whose interactions can cause failures even when each protocol works correctly. The authors aim to automatically detect a broad class of failures independent of protocol for both operational and experimental networks. They introduce Header Space Analysis, a protocol‑agnostic framework that models packet headers as bit strings in a high‑dimensional space and statically checks configurations using the Hassel tool library. Using Hassel, the authors identified all forwarding loops in the Stanford backbone in under ten minutes and verified reachability between subnets in 13 seconds, and uncovered a complex loop in an experimental loose source routing protocol in four minutes.

Abstract

Today's networks typically carry or deploy dozens of protocols and mechanisms simultaneously such as MPLS, NAT, ACLs and route redistribution. Even when individual protocols function correctly, failures can arise from the complex interactions of their aggregate, requiring network administrators to be masters of detail. Our goal is to automatically find an important class of failures, regardless of the protocols running, for both operational and experimental networks. To this end we developed a general and protocol-agnostic framework, called Header Space Analysis (HSA). Our formalism allows us to statically check network specifications and configurations to identify an important class of failures such as Reachability Failures, Forwarding Loops and Traffic Isolation and Leakage problems. In HSA, protocol header fields are not first class entities; instead we look at the entire packet header as a concatenation of bits without any associated meaning. Each packet is a point in the {0,1}L space where L is the maximum length of a packet header, and networking boxes transform packets from one point in the space to another point or set of points (multicast). We created a library of tools, called Hassel, to implement our framework, and used it to analyze a variety of networks and protocols. Hassel was used to analyze the Stanford University backbone network, and found all the forwarding loops in less than 10 minutes, and verified reachability constraints between two subnets in 13 seconds. It also found a large and complex loop in an experimental loose source routing protocol in 4 minutes.