网络验证中数据平面验证的方法与挑战网络的配置是正确的,但是人工检查过于繁琐,于是一个新的研究领域——网络验证进入了研究者的视野。网络验证是指使用数学中的形式化方法检查网络配置。网络验证可分为数据平面验证和控制平面验证。如图1[1]所示,数据平面是指网络设备中指定数据包的转发行为的功能,如转发表、流表;控制平面是指结合网络拓扑、环境信息等,生成数据平面功能,如网络设备的配置文件。本文主要介绍目前数据平面验证工具,主要参考Li[1]等人发表的综述。2019年。图1网络层次结构和常见错误ConfigChecker最早由Al-Shaer[2]于2009年提出,作为ConfigChecker的数据平面验证工具。ConfigChecker基于模型检查,是形式化验证中非常常用和重要的验证方法。ConfigChecker使用状态机对网络建模。状态机的状态由数据包的头部信息和位置决定。转发表等数据平面信息被建模为状态转换关系。不同设备的行为可以由一组规则来确定。指示每个规则都有一个条件和一个操作。条件可以表示为带有状态参数的布尔公式。如果设备上的消息满足公式,就会触发相应的动作。这个过程使用BDD(binarydecision-makingFigure)对访问控制策略进行编码,然后使用CTL(computationaltreelogic)来表示网络验证属性,比如可达性检查、环路检测、安全问题的发现,最后检查是否所有状态满足每个属性。虽然模型检查存在状态爆炸问题,基于模型检查的验证工具很难应用于大规模网络,但ConfigChecker的提出证明了使用形式化方法验证网络的可行性。看完这篇文章,我对模型检查也有了更深的理解。2011年,Mai[3]等人提出了第一个数据平面验证工具Anteater,用于真实网络中的网络验证。核心思想是将网络验证问题转化为SAT问题,然后通过SAT求解器求解。Anteater验证的主要过程比较简单:通过分析网络中的转发表得到数据面信息,将网络建模为有向图。图中的节点是网络中每个设备可能的目的地,图中的边是允许数据包经过两个节点需要满足的条件(用策略函数表示,即多个布尔公式);然后将待验证的属性用一些声明性语言(如Ruby)表达并转化为SAT公式(这个过程需要通过两边策略函数的组合得到一个SAT公式),最后,是否SAT求解器变换后的SAT公式用于验证属性是否可以满足(参考可达性验证算法的思想,计算节点间每条路径允许通过的数据包集合).我觉得本文的系统建模方法还是比较容易理解的。基于有向图,节点是位置,边是条件。节点间流动的数据包使用符号包。变量表示(包含数据包的IP地址、MAC地址、端口号等信息)。本文的网络属性验证基本围绕可达性验证算法展开。可达性算法的思想是,如果判断s和t的可达性,就是判断是否存在满足从s到t的路径的符号包。在所有边上做约束,把这些条件组合成一个SAT公式,然后求解。转发周期验证是为每个顶点v添加一个虚拟节点v',然后分别验证v-v'的可达性。丢包验证是在网络中加入一个汇聚节点d,假设它可以到达任何目的地,然后分别测试每个节点v的v-d可达性。一致性验证就是分别验证这两个节点和其他节点的可达性和丢包,然后求异或(即看结果是否相同)。虽然Anteater不能进行实时验证,扩展性和时间效率也不够好,但我认为使用可达性验证算法来计算数据包是非常有意义的,并且在后续的工具中也应用了这个思想。HSAKazemian[4]等人在2012年提出了HSA(HeaderSpaceAnalysis),它基于符号执行技术。与之前的食蚁兽完全不同。HSA比较抽象,比较难理解。HSA的系统建模过程很复杂:有七个部分需要注意。(1)文章提出了头部空间(HeaderSpace)H的概念,把头部看成一个由0和1组成的序列,在{0,1}L(L表示序列长度)头部空间中,一个头部是一个点,一条流是一个区域。(2)将每个网络设备的每个输入端口可能输入的所有header组合成一个网络空间N(即headerspaceH×{alldeviceinputports})。(3)每个网络设备根据其功能定义不同的网络传输函数。该函数有两个参数,分别是header和port端口。该函数定义了经过某个网络设备后,头空间中不同区域的转换。(4)定义拓扑传递函数。该函数的参数与网络传输函数的参数相同(header,port)。该函数用于描述网络中的每条链路。通常,一组(header,port)经过网络传递函数的转换后,其链路状态也会发生变化,需要一个拓扑传递函数来计算新的拓扑状态。(5)定义了Slice三元组(网络空间N的子集,读写操作,以及Slice的所有传递函数)。我认为Slice的主要功能是描述数据包的集合,这和符号包(symbolicpacket)功能类似。(6)定义了头部空间的代数,因为每个数据包(或流)都是头部空间中0和1的组合,交、并、补、差、T(传递函数可以输出(header,port)set)和T-1等操作用于对头部空间中的子空间进行操作,得到最终的空间(即剩余的数据包)。(7)网络设备建模,将不同网络设备的多个传输函数按照其功能进行组合,得到一个总的函数,如路由器处理数据包的过程为改写源地址和目的地址(T1),减少TTL(T2),更新校验和(T3),并转发到出端口(T4),路由器满足以上四个转换函数就可以得到Trouter=T1(T2(T3(T4(header,port))))。网络验证是将网络属性建模到头部空间的相关断言中。验证过程是先根据断言构造一个特定的符号包几何结构,分析输入网络的传递函数,然后通过分析传递函数来分析符号包集合。处理确定断言的满意度以完成属性验证。由于使用基于函数的分析方法,可以找到所有违反验证属性的反例。可达性分析,如图2[4]所示,是考虑所有远离源地址的头部空间。在到达目的地址的过程中,跟踪这段空间(中间会经历很多传递函数,空间会减少),到达目的地址,如果头空间有剩余,则可达,并且然后根据上面提到的T-1(传递函数的逆函数)函数找到源地址发送的可以到达目的地址的头集合。环路检测是在每个端口输入一个全是x(wildcard)的测试头来跟踪数据包。如果数据包返回到源端口,则说明存在环路。图2计算a到b可达性示意图。我觉得HAS比Anteater更难理解,但是提出的headerspace很巧妙。数据包作为点,网络设备作为点与点之间的链接。线(与食蚁兽相反:设备地址是点,数据包是线)。这种抽象可以在一定程度上使复杂的网络空间变得更简单。VeriFlow[5]于2013年提出,是第一个用于数据平面实时验证的工具。某种程度上,VeriFlow在Anteater的基础上增加了增量计算,实现了实时验证,因为VeriFlow也是基于可达性算法,对数据包进行计算。VeriFlow的总体思路是:实时监控SDN网络中的所有网络更新事件,VeriFlow处于控制器和网络设备之间的夹层;然后VeriFlow被设计为在受网络更新影响的小范围内进行网络验证,验证过程使用自定义算法。VeriFlow仅在小范围内实现验证:通过分析SDN控制器发布的新规则,根据新规则和与新规则重叠的旧规则,将网络划分为一组等价类,每次网络更新只会影响少数等价类,然后为每个修改后的等价类构建自己的转发图。转发图用于表示网络的转发行为,最终通过遍历转发图来检查网络属性。由于VeriFlow只进行小规模验证,验证速度非常快,基于等价类实现了实时验证的目的。等价类的划分就是将网络中具有相同转发行为的数据包集合划分为一个等价类。为了加快等价类的划分,找到受更新影响的等价类,本文采用多维前缀树(trie)。这种数据结构适用于数据包分类算法。trie中的每一层对应于转发规则中的特定位。trie的每个节点都有1、0、x三个分支。一个trie可以看做是若干次trie或若干维的组合,每个维对应数据包头中的A字段,trie的根到叶节点的路径代表匹配规则的数据包集合,以及每个叶子节点存储匹配数据包集的规则及其位置,从而完成等价类划分,如图3所示[5]。划分等价类后,为每个等价类生成一个转发图。转发图用于表示等价类中的数据包是如何转发的。图中的节点代表特定网络设备的等价类。方向侧表示(等价类,设备)对的转发规则。如果图中两个节点X和Y相连,则表示根据节点X所在设备的转发表,该等价类的数据包可以发送到Y所在设备。在设备中。构建转发图的过程需要再次遍历trie,以找到匹配等价类的数据包和规则。网络属性的校验基于转发图,将校验属性设置为验证函数,以转发图为输入,执行函数,得到结果。VeriFlow开发了一个编程接口,用于编写和插入新的属性检查函数。在VeriFlow中,可达性验证、环路验证、一致性验证等都是通过编写具体的函数来完成的。图3VeriFlow计算等价类的过程数据平面实时验证工具NetPlumber[6]也出现于2013年,主要用于SDN网络。在SDN网络中,控制器向每个网络设备发送各种规则,NetPlumber在控制器和设备之间检查这些规则。它首先继承了HSA的思想,借助于头部空间的思想,将一个数据包看成是头部空间中的一个点,将一组数据包看成一个区域,将网络设备定义为不同的传递函数,完成数据包在头部空间的流动。本文对传递函数的介绍比较清楚:每个传递函数由一系列规则组成,一个规则包括一组输入端口、一个通配符表达式(用于过滤数据包)和一组与表达式匹配的数据包操作、操作包括转发、删除、重写、封装等。NetPlumber对HSA的改进主要体现在实时增量检查的实现和新的属性检查方法上。这样在HSANetPlumber中可以检查的属性就可以完成了。NetPlumberNetPlumber的核心是首先通过每个转发表构造一个依赖图,称为管道图,如图4所示[6],然后通过分析SDN控制器发布的规则来调整图。图中的节点对应于规则,图中的有向边称为管道,对应于规则之间的依赖关系,表示匹配数据包的可能路径。定义每个管道边缘以包含用于过滤数据包的管道过滤器。这篇文章中规则(节点)的定义也很巧妙,定义为一个二元组,match字段用来标识规则可以处理的数据包,action字段表示对这些数据的操作数据包。在管道图中,如果两个规则节点相连,一个是两个规则所属的网络设备之间可能存在物理链路,另一个是第一个规则节点处理的数据包可能被识别由第二个规则节点处理。文章介绍了规则增删改查和链接增删改plumbinggraph的更新方法。该内容也是NetPlumber进行实时验证的依据。每次网络变化,管道图不会重新建立,只是小规模更新,计算速度快,实现实时更新。文章中提到的一个对实时网络更新也有帮助的想法是分布式NetPlumber,它将管道图划分为多个集群,一个集群中的节点交互更多,集群之间共享的节点被复制到另一个集群中。那么每个cluster可以同时计算,速度更快。图4.由4个交换机组成的简单网络的管道图。NetPlumber中的所有属性验证也是基于管道图的检测。通过在图中指定位置添加探测节点来收集数据包并进行验证,每个探测节点都定义了一个过滤表达式和一个测试表达式,过滤表达式用于过滤数据包,测试表达式用于验证属性。例如计算端口s到端口d的可达性,向s中注入一组全为x通配符的数据包,使其沿着所有有向边传播。在每个规则节点上,通过匹配过滤流,并通过动作转换后,得到一个新的流,继续传递到下一个节点。如果d处有来自s的数据包,则说明s和d可达。我觉得NetPlumber的整体思路可以分为两部分。一种是在头部空间中表示整个网络,另一种是从头部空间中获取管道图,通过验证管道图中的节点来完成属性验证。借助管道图的巧妙设计,可以实时验证数据平面,检测所有与网络状态更新相关的网络属性验证。同时可以对图进行聚类和划分,实现并行计算。小结目前介绍了几种常用的数据平面验证工具,包括ConfigChecker、Anteater、HSA、VeriFlow、NetPlumber。数据平面验证基本上基于Xie[7]提出的可达性算法。通过计算一条路径上的数据包,如果结果不为空,则表示可达。不同的工具也有自己的特点和有价值的想法。下面简单总结一下:(1)ConfigChecker基于符号模型检测技术,根据数据包头信息和位置建模为状态,用BDD表示的布尔公式表示状态转移关系,使用CTL来表达验证属性,通过遍历所有状态来验证属性。(2)基于SAT问题,Anteater根据数据平面信息将网络构造成有向图。节点代表位置,有向边代表数据包通过的条件(策略),用布尔公式对网络进行编码。数据包由数据包头域中的一组变量符号表示,然后将验证属性表示为SAT实例,由SAT求解器进行验证。(3)基于符号执行技术,HSA提出了headspace的概念,一个数据包是headspace中的一个点,对headspace中的区域进行过滤就是对数据包的过滤。不同设备的能力被定义为用于在顶部空间区域上操作的传递函数。属性验证过程是将不同的属性作为不同的断言写在头空间中,通过判断断言的真假来验证属性。(4)VeriFlow基于等价类的思想实现实时验证。VeriFlow通过监控SDN网络中控制器与网络设备之间的通信,将具有相同转发行为的数据包划分为一个等价类,该类构建一个转发图,其中节点代表网络设备,边代表设备的转发规则.基于图算法对每个等价类的转发图进行属性校验。(5)基于增量计算的思想,NetPlumber在完成数据包到HSA中头部空间的映射后,构建了一个依赖图,称为plumbinggraph。节点代表规则,边代表规则之间的依赖关系。通过在plumbinggraph中添加检测节点,然后根据检测节点完成相应的属性校验(带过滤表达式和测试表达式)。数据平面可以在网络当前时刻完成网络验证,只有在网络配置完成后网络真正运行时才能检测到。错误无法提前检查,所以网络验证未来的发展方向仍然需要关注控制平面,但是本文中的数据平面验证工具也起到了重要的作用,因为很大一部分控制平面验证工具首先生成通过一些方法根据网络设备的控制平面信息生成数据平面,然后对生成的数据平面进行数据平面验证。验证,这个验证过程同样需要数据平面验证工具。综上所述,可以看出在网络验证领域的数据平面验证中出现了很多巧妙的验证思想和工具,为网络验证更好的发展奠定了基础。参考文献[1]LiYH,YinX,WangZL,etal.ASurveyonNetworkVerificationandTestingWithFormalMethods:ApproachesandChallenges.IEEECommunicationsSurveys&Tutorials,2019,21(1):940-969.[2]Al-ShaerE,MarreroW,El-AtawyA,等。盒子中的网络配置:网络可达性和安全性的端到端验证。载于:2009年第17届IEEE网络协议国际会议,2009:123-132。[3]MaiH、KhurshidA、AgarwalR等。使用anteater调试数据平面。在:ACMSIGCOMM2011会议论文集,2011:290-301。[4]KazemianP、VargheseG、MckeownN.Headerspaceanalysis:Staticcheckingfornetworks。在:第9届USENIX网络系统设计与实现会议论文集,2012:9.[5]KhurshidA,ZouX,ZhouW,等。VeriFlow:实时验证网络范围的不变量。在:第10届{USENIX}网络系统设计与实现研讨会({NSDI}13),2013:15-27.[6]KazemianP,ChangM,ZengH,等人。使用标头空间分析进行实时网络策略检查。见:第10届USENIX网络系统设计与实现会议论文集,2013:99-112。[7]XieGG,JibinZ,MaltzDA,等。IP网络的静态可达性分析在:IEEE计算机和通信协会第24届年度联合会议论文集,2005:2170-2183卷,您可以通过以下二维码关注和转载本文,请联系中国保密协会科学技术分会公众号。
