Header Space Analysis: Static Checking For Networks
Kazemian P, Varghese G, McKeown N. Header space analysis: Static checking for networks[C]//Presented as part of the 9th {USENIX} Symposium on Networked Systems Design and Implementation ({NSDI} 12). 2012: 113-126.
看本文原因:好多文章中的参考文献,且作者Nick是OF提出者。本文提出Header Space Analysis来分析错误类别如:Reachability Failure,Forwarding Loops,Traffic Isolation,Leakage problems。我们装将包头视作一系列位的连接,每个都是一个点,L是包头最大长度,而网络box的转换视作将点空间中的一个点转换为另一个(或一些)。
Introduction
我们的目标是:1.帮助风络管理员静态分析网络;2.保证不同集的主机,用户,流量的隔离;3.使用更通用的方式对网络切片进行静态分析。我们的关键是使用几何应用进行包分类。 首先:每个包都可以用空间中的点进行表示。 其次:将中间设备模型化为进行L维空间与子空间转换的box transfer function。如图1中的。
最后:使用作为T的总和,作为topology transfer function,至此网络行为可以用和表示。
几何模型基本介绍
header space :将包头视作为0和1组成的平坦序列,而其可视为中的一个点,L为包头长度上限,将该空间称作header space 。 不包括数据,因为假高数据不影响包的处理(如果是一个入侵检测的box,那么L就是整个包的长度),注意:不同的协议对相同的包头位具有不同的解读。
Network Space :表示为:,这里指的是网络端口,这种所有可能的头空间对应上所有可能的端口称为网络空间
Network Transfer Function :当包在网络中传输时,它将包从一个point转换到另一个point(s)。所有的网络boxes可以视作为Transfer Function T,而T作用是将从端口p到达的头h映射:$T(h, p) : \quad(h, p) \rightarrow\left{\left(h_{1}, p_{1}\right),\left(h_{2}, p_{2}\right), \ldots\right}$,而就是所有T组成的一个组合函数,表示为: $\Psi(h, p)=\left{\begin{array}{ll}{T_{1}(h, p)} & {\text { if } p \in \text { switch }{1}} \ {\cdots} & {\cdots} \ {T{n}(h, p)} & {\text { if } p \in \text { switch }_{n}}\end{array}\right.$
Topology Transfer Function :它就是一表示网络连接的函数,在一端接收包并将其发送到另一端(不作修改),这里的连接是单向的,定义为: $\Gamma(h, p)=\left{\begin{array}{ll}{\left{\left(h, p^{}\right)\right}} & {\text { if } p \text { connected to } p^{}} \ {{ }} & {\text { if } p \text { is not connected }}\end{array}\right.$
Multihop Packet Traversal:使用表示,k跳可以被表示为:或,,意为往链路上交付包,每个在box里对包进行传递。
Slice:可分为对网络空间,权限,转换函 数的切片。例如:将目的子网为192.168.1.0/24的包限制为port:1,2,3,可被表示为:
modeling Networking Boxes
本部分是对转换函数的一个说明。例:指的是对源IP,指将h的fields字段重写为values。在IPv4 router中处理包分为四步:1.重写源和目的MAC。2.减TTL。3.更新校验值。4.交付到出端口。
可表示为:。一个一个解释:表示寻找并返回output port,类似的,表示寻找next hop MAC,更新源MAC和目的MAC。对ttl的处理,为0丢弃,否则减一。也可以简化模型表示如: or even ,例如一个简化转换函数将子网S1,S2,S3的包分别交付到端口P1,P2,P3表示为: $T_{r}(h, p)=\left{\begin{array}{ll}{\left{\left(h, p_{1}\right)\right}} & {\text { if } i p_{-} d s t(h) \in S_{1}} \ {\left{\left(h, p_{2}\right)\right}} & {\text { if } i p_{-} d s t(h) \in S_{2}} \ {\left{\left(h, p_{3}\right)\right}} & {\text { if } i p_{-} d s t(h) \in S_{3}} \ {{ }} & {\text { otherwise. }}\end{array}\right.$
firewall可模型化为:抽取IP和TCP头,匹配通配符并依匹配规则进行丢弃和交付。
NAT可模型化为:一个重写操作。 模型的详细程度取决于应用需要,可以使用工具对路由配置和交付表进行自动模型建立。
Header Space Algebra
对头空间定义集合操作:intersection,union,coplementation,defference,对转换函数定义:Domaain,Range,Range Inverse。
- intersection 可表解为交
如上图,z表示空,如果有任一位为空,则结果为。例:,。这里,对每一位进行编码:0:01,1:10,x:11,z:00,这就可以用集合操作AND对头空间进行操作了。
- union 正常的并操用
- complementation:补或非,不知道该翻译为哪一个,具体操作规则为:
例:
- Difference:差, 例:
Domain,Range,Range Inverse
- Domain:是转换函数可接收的所有的(header,port)对的集合,even output is empty
- Range:所有转换函数可能输出的(header,port)对的集合。
- Range Inverse:给定一个对S:(header,port),找到所有可能产生该对的对集合X:{(header,port)},即:T(X)=S,X=TS,可称为逆
使用
Reachability Analysis
假设a到b,考虑所有可能离开a的包,跟踪它到b的所有路径并转换,到达b后看是否还有,若有,则根据路径求逆找可能的包,否则认为不可达。 用一个例子来说明:定义a到b的可达函数: $R_{a \rightarrow b}=\bigcup_{a \rightarrow b \text { paths }}\left{T_{n}\left(\Gamma\left(T_{n-1}\left(\ldots \ldots .\left(\Gamma\left(T_{1}(h, p) \ldots\right)\right)\right}\right.\right.\right.$所有可能的路径可表示为: 该可达函数的range即可从a到b的所有可能的包,可通过求逆函数来根据到达的包求从a出发的原始包: 这里的 图2是一个可达性测试例子。
最后获得的结果为:10010x10 ∪ 01011x10 复杂度分析:,d为包需要经历的最多路由个数,R为交付规则最多的路由的规则数。
Loop Detection
- 普能循环:对于一个给定的网络转换函数,通过往每个端口中注入all-x测试包并跟踪以达到测试环路目的。以下情况停止跟踪:1.包离开网络。2.包到达了之前到达过的端口。3.包到达了注入端口。仅3报告有环。图3为注入测试包示例图,图4为包跟踪图。
图4中,Hdr为当前包头,Port为当前端口,Visits:已访端口,按序。当Port中的值到Visits中每一个值相同则找到loop。 复杂度:,P是需要注入包的端口数。
- finding single infinete loops:在图3中的环:A-C-B-D-A,假设表示返回的部分头部,定义为:。则,它两有三种相关:1.,该环是有尽环。2.该环是无尽环。3.不在以上两种:让包继续包,直到以上两种之一发生。
Slice Isolation
本文方法可以:1.创建新切片并保证隔离性。2.当切片流量泄露时可检测。
-
创建新切片。两个切片的例子:a和b为网络空间的域:,其中:$N_{a}=\left{\left(\alpha_{i}, p_{i}\right)\right]{p{i} \in \mathcal{S}} } \quad, \quad N_{b}=\left{\left(\beta_{i}, p_{i}\right)\right]{p{i} \in \mathcal{S}} }\alpha,\beta\alpha_i \cap \beta_i = \phiN_{a} \cap N_{b}=\left{\left(\alpha_{i} \cap \beta_{i}, p_{i}\right)\right]{p{i} \in N_{a} & p_{i} \in N_{b}} }$找到。
-
Data leakage:即使两个切片无重叠,也有可能发生数据泄露,因为包在任何端口都有可能被重写。因此在每一个端口使用网络转换函数计算切片a头空间的逆,记为:output header set。如果这个集在任何端口与其他切片重叠,则有可能会发生数据泄露。图5为检测的图形表示。
复杂度:,W是描述切片的通配符最大表达式,N是切片网络个数。
实现
本文有源码(找了,没找到),使用python2.6编写实现称为:Hassel。图6为Hassel的block diagram。表1为5个关键优化及其影响。
评估
Verfication of an enterprise Network
拓扑图如图7。这个图之前见过,好多论文都出现过,原来是斯坦福大学的网络拓扑。
测试环路
在图7中共找到12个环路,性能总结在表中。
测试可能的配置错误
Stnaford 拥有IP:171.64.0.0/14,斯坦福丢弃所有无规则匹配的包,假设这条配置手误出错配成:171.64.0.0/16,那么就有可能在斯坦福和ISP之间来回循环包,在表2中可见这样的错误可以在10分钏之内测出。
checking slice isolation
本节创建新节片需要验证:1.不能与已存在的切片重叠;2.不能有数据泄露。图8可见切片隔离性测试结果。
图9为切片数据泄露性能测试结果
性能测试结果与复杂性分析类似,程线性,并且性能优。
结语:除此之处,该方法还适用于对新协议的测试但也有不足之处:1.可以测试出路由表不一致,但无法告诉我们原因;2.可以定位到导致问题的具体流,但无法告诉我们how or why;3.只能测试也持续时间很长的问题。
如果这篇文章帮到了你, 那就赞助我一瓶水吧, 这可以让我有动力去写更多的文章
Sponsor