前 言
现如今网络越来越越发繁杂，在营运商对网络开展配备时，一些不知不觉违反规定配备很有可能会造成大错，因而必须较大水平上确保网络的配备恰当，但人力查验又过于繁杂，因此一种新的研究领域——网络验证进入了学者的视线。网络验证指应用初中数学的流于形式方式对网络配备开展查验。网络验证可以分成数据信息平面图验证和操纵平面图验证，如下图1[1]所显示，数据信息平面图就是指网络机器设备中特定数据包的分享个人行为的作用，例如转发布、流表;操纵平面图就是指融合网络拓扑结构、自然环境信息内容等转化成数据信息平面图的作用，如网络机器设备的环境变量。文中主要是对现阶段数据信息平面图验证专用工具开展详细介绍，关键参照了Li[1]等在2019年发布的具体描述。
图1 网络结构分析和普遍不正确
ConfigChecker
早在2009年由Al-Shaer[2]最先明确提出ConfigChecker数据信息平面图验证专用工具，ConfigChecker是根据实体模型查验的，是流于形式验证中十分普遍且关键的验证方式。ConfigChecker应用有限状态机模型网络，有限状态机的情况是由数据包的头顶部信息内容和地方明确的，将由转发布等数据信息平面图信息内容模型为情况迁移关联，不一样设施的方式可以用一组标准来表明，每一个标准都是有一个标准和一个姿势，标准可以用情况中的技术参数来透露一个布尔运算公式计算，假如机器设备上的报文格式达到该公式计算，则开启相对应姿势，此环节应用了BDD(二元管理决策图)对浏览控制方法编号，随后应用CTL(测算树逻辑性)表明网络验证属性，如可达性查验、环城路检验及其发觉安全系数问题，最终查验全部情况是不是符合各属性。尽管实体模型查验存有情况爆的问题，以实体模型查验为基本的验证专用工具难以运用在大中型网络上，可是ConfigChecker的明确提出证实了应用流于形式方式验证网络的可行性分析，根据对该文章的阅读文章我就模型拟合检验拥有更快的了解。
Mai[3]等在2011年明确提出了初次在真正网络中开展网络验证的数据信息平面图验证专用工具Anteater，核心内容是将网络验证问题转换为SAT问题，随后根据SAT求得器开展求得。Anteater验证的具体步骤较简易：根据剖析网络中的转发布得到数据信息平面图信息内容，将网络模型成连通图，图上的连接点是网络中各机器设备很有可能抵达的终点，图上的边是容许在两连接点根据的数据包必须达到的标准(根据对策函数公式来表明，也就是好几个布尔运算公式计算);再将所需验证的属性应用一些申明式语言表达(如Ruby)来表明，并转化成SAT公式计算(该全过程是要根据各旁边对策函数公式的组成来获得一个SAT公式计算)，最终根据SAT求得器测算验证属性所转换的SAT公式计算是不是可达到(参照了可达性验证优化算法观念，测算连接点中间各途径容许利用的数据包结合)。我觉得该网站中系统对模型的办法是很容易了解的，根据连通图，连接点为地址，边为标准，在连接点中间流通的数据包用一种称之为标记包(symbolic packet)的自变量表明(在其中包括了数据包的IP地址、MAC地址、端口等信息内容)。文中的网络属性验证层面基本上全是紧紧围绕着可达性验证优化算法进行的，可达性优化算法观念是若判断s、t二点的可达性便是判断是不是存有symbolic packet达到从s到t的方向上全部旁边的约束方程，将这种标准合拼成一个SAT公式计算，随后求得。分享循环系统验证是为每一个端点v加一个虚似连接点v’，再各自验证v-v’的可达性。丢包率验证是网络中加上一个聚集连接点d，假定它可以抵达随意终点，随后各自检测个连接点v的v-d可达性。一致性验证是各自验证这两个连接点与其他连接点的可达性、丢包率状况，随后异中或(即看結果是不是一样)。尽管Anteater不可以开展即时验证，扩展性、時间高效率都不太好，可是我觉得这类将可达性验证优化算法用来对数据包的测算上是十分有意思的，以后的专用工具中也有运用该观念的。
HSA
Kazemian[4]等在2012年明确提出了HSA(Header Space Analysis 头数据挖掘技术技术性)，根据符号执行技术性，与先前的Anteater彻底不一样，HSA更为抽象化，不容易了解。HSA的系统软件模型全过程较繁杂：有七个必须留意的一部分。(1)文章内容明确提出了头室内空间(Header Space)H的定义，将报头当作是一组由0、1构成的编码序列，在{0,1}L(L表明编码序列长短)头室内空间中，一个报头是一个点，一个流是一片地区。(2)将每个网络机器设备的各键入端口号所很有可能键入的全部报头构成为网络室内空间N(即头空间H×{全部机器设备入端口号})。(3)将各网络机器设备按照其作用定义出不一样网络迁移函数公式，函数有两个主要参数，分别是报头header和端口号port，函数定义了头室内空间中不一样地区根据某一网络机器设备后的变换状况。(4)界定拓扑结构迁移函数公式，函数参数与网络迁移函数公式的主要参数同样(header，port)，该函数公式用以叙述网络中各链接，一般一组(header，port)经历过网络开环传递函数变换后，其链接情况也会更改，必须拓扑结构迁移函数公式来测算新的拓扑结构情况。(5)界定了Slice三元组(网络室内空间N的一个子集合，存取数据，针对该Slice的全部迁移函数公式)，我觉得Slice的首要作用便是叙述数据包结合，与Anteater中标记包(symbolic packet)作用相近。(6)界定了头室内空间的解析几何，由于每一个数据包(或流)在头室内空间是一组0、1组成，界定了交、并、补、差、T(迁移函数公式可以导出的(header，port)结合)和T-1等实际操作，用以死对头室内空间中的向量空间开展实际操作，获得最终的室内空间(即剩下的数据包)。(7)网络机器设备模型，将不一样网络机器设备按照其作用，将好几个开环传递函数组成，获得一个总的函数公式，例如无线路由器解决数据包的环节为重新写过源、目地详细地址(T1)、降低TTL(T2)、升级校验和(T3)、分享到出端口号(T4)，则该无线路由器可根据合乎以上四个迁移函数公式获得Trouter=T1(T2(T3(T4(header，port))))。
网络验证是将网络属性模型成头室内空间的有关结论，验证全过程是先依据结论结构特殊的标记数据包几何图形，键入到网络中的迁移函数公式开展剖析，随后根据剖析迁移函数公式对符号数据包结合的处理方式明确结论的达到性以进行属性验证。因为运用了根据函数公式的统计分析方法，可以寻找违背验证属性的所有反例。可达性剖析如下图2[4]所显示，是考虑到离去服务器ip的全部报头室内空间，在抵达目地详细地址的历程中，追踪这一室内空间(正中间会经过许多开环传递函数，室内空间会降低)，抵达目地详细地址时，若头室内空间也有剩下，则可达，再依据以前提及的T-1(迁移函数公式的逆)函数寻找服务器ip推送的可以抵达目地详细地址的报头结合。循环系统检验是根据给每一个端口号键入一个都是x(使用通配符)的检测报头，跟踪数据包，假如数据包回到源端口号，则表明有循环系统。
图2 测算从a到b的可达性平面图
我觉得HAS相比于Anteater更难了解一些，可是明确提出的头室内空间是十分恰当的，以数据包为点，以网络机器设备为点与点中间的线(与Anteater恰好反过来：以机器设备详细地址为点，以数据包为线)，这类抽象化在一定水平上能让繁杂的网络室内空间显得更简易。
于2013年被提到的VeriFlow[5]是第一个的对数据信息平面图开展即时验证的专用工具。VeriFlow在某种意义上是在Anteater的根基上提升了增加量测算，完成即时验证，由于VeriFlow也是根据可达性优化算法，对数据包开展测算。VeriFlow的大概观念是：实时监控系统SDN网络中任何的网络升级时事情，VeriFlow处在控制板与网络机器设备的隔层中;随后VeriFlow致力于受网络升级危害的小区域内开展网络验证，验证全过程应用自定优化算法。VeriFlow完成只在小区域内开展验证的办法是：根据剖析SDN控制板下达的新标准，根据新标准和与新规则有重合一部分的老标准，将网络区划为一组等价类，每一次网络升级只能危害一小部分等价类，随后为每一个被改动的等价类搭建不同的分享图，转发图用以表明网络的分享个人行为，最终根据解析xml分享图来查验网络属性。因为VeriFlow只开展小范畴验证，因此验证速率迅速，进而根据等价类完成了即时验证的目地。在其中等价类的区分是将网络中具备同样分享个人行为的数据包结合划为一个等价类，为了更好地加快等价类的区分和寻找受升级危害的等价类，原文中应用多维度前缀树(trie)这类适用包随机森林算法的算法设计。trie中的每一层相匹配于分享标准中的特殊位，trie的每一个连接点存有1，0，x三个支系，一个trie可以看成是好多个trie或几个层面的组成，每一个层面相匹配数据包头里的一个字段名，从trie的根到叶子节点的途径表明与该标准配对的包集，每一个叶子节点储存了配对数据包集的标准和他们所在的部位，从而完成了等价类的区划，如下图3[5]所显示。等价类区划后是为每一个等价类都转化成一个分享图，转发图是用以表明等价类中的数据包是怎样被分享的，图上连接点表明特殊网络机器设备的等价类，有向边表明针对该(等价类，机器设备)对的分享标准，若图上两连接点X，Y相接表明依据连接点X所属机器设备的转发布，该等价类中的数据包可以发送至Y所属的设施中。搭建分享图的全过程为了更好地寻找与等价类配对的包和标准，必须再度解析xmltrie。网络属性的检验是构建在分享图上的，将查看的属性设置为一个验证函数公式，将分享图做为键入，实行函数公式，获得結果。VeriFlow开发设计了一个可编插口，用以撰写和插进新的属性查验函数公式。在VeriFlow中可达性验证、循环系统验证、一致性验证等全是根据撰写特殊函数公式进行的。
图3 VeriFlow测算等价类的全过程
数据信息平面图即时验证专用工具NetPlumber[6]一样发生于2013年，主要是运用在SDN网络中。SDN网络中主要是根据控制板向各计算机设备推送各种各样规则，而NetPlumber便是处在控制板和机器设备中间，对这种规则开展查验。它最先是拥有了HSA的观念，依靠了头室内空间的观念(header space)，将一个报文格式当作头室内空间的一个点，将一组报文格式当作一片地区，将计算机设备界定为不一样迁移函数公式，进行数据包在头室内空间的流动性。本文中更清晰地讲解了迁移函数公式：每一个迁移函数公式由一些列规则组成，一个规则包含一组键入端口号、一个使用通配符关系式(用以过虑数据包)和一组对合乎关系式的数据包的实际操作，操作包含分享、删掉、重新写过、封装形式等。NetPlumber针对HSA的改善关键反映在保持了即时增加量定期检查明确提出了一种新的属性查验方法。因此HSA中可以查验的属性NetPlumber都能够进行。
NetPlumber
NetPlumber的核心内容是最先根据各转发布搭建了一种依赖图，称为plumbing graph，如下图4[6]所显示，随后再根据剖析SDN控制板下达的规则对该图开展调节，在其中图的节点相匹配规则，图的有向边称之为pipes，相匹配了规则中间的相互依赖，意味着了配对数据包的很有可能途径。界定每一个pipe边包括一个pipe fliter，用以过虑数据包。原文中对规则(节点的理解也是十分恰当的，界定为一个二元组，match字段名用以标志出可以受该规则解决的数据包，action字段名表明对这种数据包的实际操作。在plumbing graph中若两规则节点相接，一是很有可能这两个规则隶属的计算机设备中间存有物理学链接，二是很有可能被第一个规则节点解决后的数据包可以被第二个规则节点鉴别并再开展解决。针对规则的提升、删掉和链接的提升、删掉原文中都详细介绍了怎样对plumbing graph开展升级，该內容也是NetPlumber可以开展即时验证的基本，每一次互联网产生变化时，不容易再次创建plumbing graph，而仅仅小区域的升级，处理速度较快，以完成自动更新。原文中提及的还有利于即时互联网升级的一个观念是分布式系统NetPlumber，将plumbing graph分为好几个群集，一个集群内的节点互动大量，群集间的同用节点复制一个划归另一个群集，随后各群集中间可以与此同时测算，速率更快。
图4 由4个网络交换机构成的简单网络的plumbing graph
NetPlumber中的全部属性验证也是根据对plumbing graph开展检验的，根据向图上特定部位提升probe nodes搜集数据包，开展验证，界定每一个probe node、具备一个过虑关系式和一个检测关系式，过虑关系式用以过虑数据包，检测关系式用以验证属性。例如测算端口号s到端口d的可进入性，向s引入一个都是x使用通配符的一组数据包，使其顺着全部的有向边散播，在每一个规则节点上，flow由match过虑，由action变换后获得一个新的flow，再次传入下一个节点，假如在d处存有来源于s的数据包，则表明s和d可达。我觉得NetPlumber的总体设计构思可以分成两一部分，一是将全部互联网都表达在头室内空间中，二是由头空间获得plumbing graph，根据对plumbing graph中节点的验证以进行属性验证。依靠plumbing graph这一恰当的设计最先完成了即时验证数据信息平面，还能够检验一切由网络状态升级有关的互联网属性验证，与此同时可以对graph开展聚类分析的区划完成并行处理。
小 结
现阶段已完成了好多个较为普遍的数据信息平面验证专用工具的详细介绍，包含ConfigChecker、Anteater、HSA、VeriFlow、NetPlumber。数据信息平面验证基本上全是根据Xie[7]明确提出的可进入性优化算法，根据对一条途径中的数据包开展测算，結果不以空则说明可达。不一样专用工具也是有自己的特性和有使用价值的观念，下边开展简短的汇总：(1)ConfigChecker根据标记实体模型无损检测技术，依据数据包头信息内容和所在部位模型为情况，应用BDD表述的布尔运算公式计算表明情况迁移关联，应用CTL表述验证属性，根据解析xml全部的情况来验证属性。(2)Anteater根据SAT问题，依据数据信息平面信息内容将互联网搭建成一个连通图，节点表明部位，有向边表明数据包根据的标准(对策)，将互联网用布尔运算公式计算编号。用一组表明数据包头字段名的自变量的标记包示数据包，再将验证属性表明成一个个SAT案例，根据SAT求得器开展验证。(3)HSA根据符号执行技术性，明确提出头室内空间的定义，一个数据包为头室内空间中的一个点，死对头室内空间中地区的过虑便是对数据包的过虑。将不一样设施的作用界定为迁移函数公式，用以死对头室内空间的范围实现实际操作。属性验证全过程是将不一样属性写出头室内空间内的不一样结论，根据判断结论的真伪来验证属性。(4)VeriFlow根据等价类观念完成了即时验证，它根据监管SDN互联网中控制板与计算机设备间的通讯，将具备同样分享个人行为的数据包划为一个等价类，再为每一个等价类创建一个分享图，节点意味着计算机设备，边意味着该专用设备的分享规则。属性查验是在每个等价类的分享图上根据图算法开展验证。(5)NetPlumber根据增加量测算的观念，在进行HSA里将数据包投射停止室内空间后，把互联网完工了一种称为plumbing graph的依赖图，节点表明规则，边表示规则间的相互依赖，根据在plumbing graph中提升检测节点，随后依据检测节点(含有过虑关系式和检测关系式)进行相对应属性验证。
数据信息平面可以进行互联网现阶段这一时时刻刻的互联网验证，而且只有在网络配置进行后真真正正运作互联网发生失误时才可以检验出去，不可以对不正确开展提早查验，因此将来互联网验证的发展前景或是必须聚集在操纵平面上，但文中数据信息平面验证专用工具也很都起着至关重要的功效，由于有挺大一部分操纵平面验证专用工具是先根据一些方式依据计算机设备操纵平面信息内容转化成数据信息平面后，再对转化成的数据信息平面开展验证，这一验证全过程也是必须数据信息平面验证专用工具的。综上所述可以看得出互联网验证行业的数据信息平面验证发生了许多精妙的验证观念和专用工具，为互联网验证更强的进步打下了基本。
论文参考文献
[1]Li Y H, Yin X,Wang Z L, et al. A Survey on Network Verification and Testing With FormalMethods: Approaches and Challenges.IEEE Communications Surveys & Tutorials,2019, 21(1): 940-969.
[2]Al-Shaer E,Marrero W, El-Atawy A, et al. Network configuration in a box: towardsend-to-end verification of network reachability and security. In: 2009 17thIEEE International Conference on Network Protocols, 2009: 123-132.
[3]Mai H, KhurshidA, Agarwal R, et al. Debugging the data plane with anteater. In: Proceedings ofthe ACM SIGCOMM 2011 conference, 2011: 290-301.
[4]Kazemian P,Varghese G, Mckeown N. Header space analysis: Static checking for networks. In:Proceedings of the 9th USENIX conference on Networked Systems Design andImplementation, 2012: 9.
[5]Khurshid A, ZouX, Zhou W, et al. VeriFlow: Verifying Network-Wide Invariants in Real Time. In:10th {USENIX} Symposium on Networked Systems Design and Implementation ({NSDI}13), 2013: 15-27.
[6]Kazemian P,Chang M, Zeng H, et al. Real time network policy checking using header spaceanalysis. In: Proceedings of the 10th USENIX conference on Networked SystemsDesign and Implementation, 2013: 99–112.
[7]Xie G G, JibinZ, Maltz D A, et al. On static reachability analysis of IP networks. In:Proceedings IEEE 24th Annual Joint Conference of the IEEE Computer andCommunications Societies., 2005: 2170-2183 vol. 3.
文中摘自微信公众平台「我国信息保密研究会科技进步联合会」，可以利用下面二维码关心。转截文中请联络我国信息保密研究会科技进步联合会微信公众号。
