[关闭]
@EggGump 2019-04-17T10:41:05.000000Z 字数 5899 阅读 1048

Header Space Analysis: Static Checking For Networks

security

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中的AjnvGR.png
最后:使用作为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组成的一个组合函数,表示为:

Topology Transfer Function :它就是一表示网络连接的函数,在一端接收包并将其发送到另一端(不作修改),这里的连接是单向的,定义为:

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表示为:

firewall可模型化为:抽取IP和TCP头,匹配通配符并依匹配规则进行丢弃和交付。
NAT可模型化为:一个重写操作。
模型的详细程度取决于应用需要,可以使用工具对路由配置和交付表进行自动模型建立。

Header Space Algebra

对头空间定义集合操作:intersection,union,coplementation,defference,对转换函数定义:Domaain,Range,Range Inverse。

Domain,Range,Range Inverse

使用

Reachability Analysis

假设a到b,考虑所有可能离开a的包,跟踪它到b的所有路径并转换,到达b后看是否还有,若有,则根据路径求逆找可能的包,否则认为不可达。
用一个例子来说明:定义a到b的可达函数:
所有可能的路径可表示为:
该可达函数的range即可从a到b的所有可能的包,可通过求逆函数来根据到达的包求从a出发的原始包:
这里的
图2是一个可达性测试例子。AvwbtA.md.png
最后获得的结果为:10010x10 ∪ 01011x10
复杂度分析:,d为包需要经历的最多路由个数,R为交付规则最多的路由的规则数。

Loop Detection

Slice Isolation

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

实现

本文有源码(找了,没找到),使用python2.6编写实现称为:Hassel。图6为Hassel的block diagram。表1为5个关键优化及其影响。
AvIoFI.md.png
AvITYt.png

评估

Verfication of an enterprise Network

拓扑图如图7。这个图之前见过,好多论文都出现过,原来是斯坦福大学的网络拓扑。
AvoUht.md.png
运行Hassel,测量性能。

测试环路

在图7中共找到12个环路,性能总结在表中。
Av7BwQ.md.png

测试可能的配置错误

Stnaford 拥有IP:171.64.0.0/14,斯坦福丢弃所有无规则匹配的包,假设这条配置手误出错配成:171.64.0.0/16,那么就有可能在斯坦福和ISP之间来回循环包,在表2中可见这样的错误可以在10分钏之内测出。

checking slice isolation

本节创建新节片需要验证:1.不能与已存在的切片重叠;2.不能有数据泄露。图8可见切片隔离性测试结果。Av7xTH.png
图9为切片数据泄露性能测试结果
AvHW9I.png
性能测试结果与复杂性分析类似,程线性,并且性能优。

结语:除此之处,该方法还适用于对新协议的测试但也有不足之处:1.可以测试出路由表不一致,但无法告诉我们原因;2.可以定位到导致问题的具体流,但无法告诉我们how or why;3.只能测试也持续时间很长的问题。

添加新批注
在作者公开此批注前,只有你和作者可见。
回复批注