Header Space Analysis: Static Checking for Networks

NSDI 2012

Problem

• Today's networks typically deploy dozens of protocols and mechanisms simultaneously (e.g. MPLS, NAT, ACLs) and route redistribution. Failures can arise from complex interactions of their aggregate, making it daunting to operate a large network today.

Insight

• The goal of this paper is to help system administrators statically analyze production networks today.

• The paper proposes a general framework, Header Space Analysis, which provides a set of tools and insights to model and check networks for a variety of failure conditions in a protocol-independent way. The key insight is a generalization of the geometric approach to packet classification, in which classification rules over K packet fields are viewed as subspaces in a K dimensional space.

Key Strength

• The insights of building header space framework on a geometric model is very interesting. The paper defines a series of main geometric spaces that abstract important components for modeling the network

• The paper solves several classical networking problem in a protocol-agnostic way with their approach.

Key Weakness

• HSA can indicate that something is broken, but it isn't able to inform the reasonings about why something was inserted or how they will be evolved as more future messages arrive. Also HSA offers no clues about efficiency of whether a specific objectives of the designers are met.

• HSA does not deal well with the churn of network, except to periodically run it based on snapshots.

• The evaluations are done on Stanford's backbone network, which is not particularly large-scale. The performance and scalability of this analysis method needs to be further verified on larger network.

• Performance optimizations on prototype are covered briefly in the conclusions. Would like to see these discussions in more details.

Comments