Header space analysis: static checking for networks

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