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 ReachabilityFailures, 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.
阅读笔记：
有一种论文，看似得来轻松，却是功到自然；看似设计简单，却是大巧不工。这样的文章一出，即便学霸、专家看了，也往往觉得眼前一亮。倘若又能联系实际，碰巧解决一两个工程问题，那就更加站得住脚了，哪怕顶级会议也是问题不大。msra的Chuanxiong Guo曾发过一些类似风格的文章，后来功力日深，不常走这类轻巧路线了。
今天读的这篇论文，无疑可称得上精妙。
sdn的概念提出早期，大家一起讨论，这玩意能干啥，当时就有人提出能做diagnosis，大家的思路就是说一旦发生了问题，通过计算能快速的发现或者解决问题。这样的工作现在也有一些成果，但都是靠solid的设计和实现取胜。这篇文章中要解决的问题，则更加大胆。给我你的网络配置（转发策略等）情况，我能告诉你有哪些问题，比如，网络中是否存在环路？并给其了一个好听的名字，叫做Header Space Analysis (HSA)。
问题提出，先别看别人咋做的，自己想一想，要解决这个问题其实技术上来说并无太大难度，如果能拿到所有节点的配置，把所有可能情况遍历一遍即可。这样做，就落入传统的解决工程问题的一般套路了。能否拔高点？这也是本文最大的亮点。网包在网络中转发，无非就是个空间变换。包头104位（5元），最多就是104维嘛。转发无非就是从一个子空间，映射到了另一个子空间。先别管这样直接粗糙的定义是否合适，但问题一下子便拔高了，有了数学上的意义。然后再自然的定义一些基本概念，一个很好的数学问题便被提出了。
之后，文章中还实现了一些简单的工具，并分析了实际的一个网络，用这些工具发现的一些可能的问题。当然，这些问题可能只是在理论意义上存在的。有理有据，这正是大家写论文该模仿的典范！
当然，原创性太强的工作，自然解决的不会那么完美，仍有很多坑等着大家去继续深入。
比如：
目前只能分析static的情况；
只能解决映射到一个点的问题；
计算复杂度如何快速降低？
能否扩展到考虑payload的情况。
解决了这些问题，这种分析的方法才会有更多的实践意义，才会被用到更多的领域，特别是安全领域。
