Header Space Analysis: Static Checking For Networks

SuperEgg included in category 科研学习

2019-09-06 2022-08-22 4047 words 9 minutes

Contents

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。我们装将包头视作一系列位的连接,每个都是一个${0,1}^L$点，L是包头最大长度，而网络box的转换视作将点空间中的一个点转换为另一个（或一些）。

Introduction

我们的目标是：1.帮助风络管理员静态分析网络；2.保证不同集的主机，用户，流量的隔离；3.使用更通用的方式对网络切片进行静态分析。我们的关键是使用几何应用进行包分类。首先：每个包都可以用${0,1}^L$空间中的点进行表示。其次：将中间设备模型化为进行L维空间与子空间转换的box transfer function。如图1中的$T_A()和T_B()$。

最后：使用$\Psi$作为T的总和，$\Gamma$作为topology transfer function，至此网络行为可以用$\Psi$和$\Gamma$表示。

几何模型基本介绍

header space $\mathcal{H}$:将包头视作为0和1组成的平坦序列，而其可视为${0,1}^L$中的一个点，L为包头长度上限，将该空间称作header space $\mathcal{H}$。 $\mathcal{H}$不包括数据，因为假高数据不影响包的处理(如果是一个入侵检测的box，那么L就是整个包的长度)，注意：不同的协议对相同的包头位具有不同的解读。

Network Space $\mathcal{N}$:表示为：${0,1}^{L} \times{1, \ldots, P}$，这里${1, \dots, P}$指的是网络端口，这种所有可能的头空间对应上所有可能的端口称为网络空间$\mathcal{N}$

Network Transfer Function $\Psi()$:当包在网络中传输时，它将包从一个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}$，而$\Psi(.)$就是所有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()$:它就是一表示网络连接的函数，在一端接收包并将其发送到另一端（不作修改），这里的连接是单向的，定义为： $\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:使用$\Phi(.)=\Psi(\Gamma(.))$表示,k跳可以被表示为：$\Psi(\Gamma(\ldots(\Gamma(h, p) \dots)$或$\Phi^{k}(h, p)$,，意为$\Gamma$往链路上交付包，每个$\Psi$在box里对包进行传递。

Slice:可分为对网络空间，权限，转换函数的切片。例如：将目的子网为192.168.1.0/24的包限制为port:1,2,3，可被表示为：$((ip_dist(h)=192.168.1.x,p\in{1,2,3}),rw,\Psi_s)$

modeling Networking Boxes

本部分是对转换函数的一个说明。例：$ip_src(h)$指的是对源IP，$\mathcal{R}(h,fields,values)$指将h的fields字段重写为values。在IPv4 router中处理包分为四步：1.重写源和目的MAC。2.减TTL。3.更新校验值。4.交付到出端口。

可表示为：$T_{I P v 4}( .)=T_{f w d}\left(T_{c h k s u m}\left(T_{t t l}\left(T_{m a c}( .)\right)\right)\right)$。一个一个解释：$T_{fwd}(h,p)$表示寻找$ip_dst(h)$并返回output port，类似的，$T_{mac}(.)$表示寻找next hop MAC，更新源MAC和目的MAC。$T_{ttl}(.)$对ttl的处理，为0丢弃，否则减一。也可以简化模型表示如：$T_{I P v 4}( .)=T_{f w d}\left(T_{t t l}( .)\right)$ or even $T_{I P v 4}( .)=T_{f w d}( )$，例如一个简化转换函数将子网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。

$\mathcal{H}操作$

intersection 可表解为交

如上图，z表示空，如果有任一位为空，则结果为$\phi$。例：$1100\mathrm{xxxx} \cap \mathrm{xx}00010\mathrm{x}=1100010\mathrm{x} $,$1100\mathrm{xxxx}\cap 111001\mathrm{xx}=11\mathrm{z}001\mathrm{xx}=\phi$。这里，对每一位进行编码：0：01,1：10,x:11,z:00，这就可以用集合操作AND对头空间进行操作了。

union 正常的并操用
complementation:补或非，不知道该翻译为哪一个，具体操作规则为：

例：$(100\mathrm{xxxxx})’=0\mathrm{xxxxxxx} \cup \mathrm{x}1\mathrm{xxxxxx} \cup \mathrm{xx}1\mathrm{xxxxx}$

Difference:差，$A-B=A\cap B’$ 例：

Domain,Range,Range Inverse

Domain:是转换函数可接收的所有的(header,port)对的集合，even output is empty
Range:所有转换函数可能输出的(header,port)对的集合。
Range Inverse:给定一个对S:(header,port)，找到所有可能产生该对的对集合X:{（header,port）}$_n$,即：T（X）=S,X=T$^{-1}$S,可称为逆

使用

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.$所有可能的路径可表示为：$a \rightarrow S_{1} \rightarrow \ldots \rightarrow S_{n-1} \rightarrow S_{n} \rightarrow b$ 该可达函数的range即可从a到b的所有可能的包，可通过求逆函数来根据到达的包求从a出发的原始包：$h_{a}=T_{1}^{-1}\left(\Gamma\left(\ldots\left(T_{n-1}^{-1}\left(\Gamma\left(T_{n}^{-1}((h, b)) \dots\right)\right)\right.\right.\right.$ 这里的$\Gamma=\Gamma^{-1}$ 图2是一个可达性测试例子。

最后获得的结果为：10010x10 ∪ 01011x10 复杂度分析：$O(dR^2)$,d为包需要经历的最多路由个数，R为交付规则最多的路由的规则数。

Loop Detection

普能循环：对于一个给定的网络转换函数，通过往每个端口中注入all-x测试包并跟踪以达到测试环路目的。以下情况停止跟踪：1.包离开网络。2.包到达了之前到达过的端口。3.包到达了注入端口。仅3报告有环。图3为注入测试包示例图，图4为包跟踪图。

图4中，Hdr为当前包头，Port为当前端口，Visits:已访端口，按序。当Port中的值到Visits中每一个值相同则找到loop。复杂度：$O(dPR^2)$，P是需要注入包的端口数。

finding single infinete loops:在图3中的环：A-C-B-D-A，假设$h_{ret}$表示返回$A_1$的部分头部，$h_{orig}$定义为：$h_{\text {orig}}=\Phi^{-1}\left(\Phi^{-1}\left(\Phi^{-1}\left(\Phi^{-1}\left(h_{\text {ret}}, A_{1}\right)\right)\right)\right)$。则，它两有三种相关：1.$h_{r e t} \cap h_{o r i g}=\phi$，该环是有尽环。2.$h_{r e t} \subseteq h_{o r i g} :$该环是无尽环。3.不在以上两种：让包继续包，直到以上两种之一发生。

Slice Isolation

本文方法可以：1.创建新切片并保证隔离性。2.当切片流量泄露时可检测。

创建新切片。两个切片的例子：a和b为网络空间的域：$N_a,N_b \in \mathcal{N}$,其中：$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$为headers. 当两个切片无重叠时，$\alpha_i \cap \beta_i = \phi$。当有重叠时，可以通过$N_{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为检测的图形表示。