成功的Python环境的4个基本工具

总 结

网络验证的目的是保证网络按照高级策略意图忠实的运行，即网络真实行为与策略一致。本文主要对网络验证中的控制平面验证和数据平面验证两个方向中的现有研究进行了简单概述。整体上来看，工具大多是基于形式化方法实现的，如基于SMT/SAT求解器的Minesweeper、Batfish、Anteater、NOD、SecGuru;基于符号执行的HSA。其他工具如rcc、ARC、ERA通过不同的建模方法实现了验证。上述工具的特点是基于模型的形式化验证，本质上是一种状态机验证技术。其大致框架如图2所示，首先将平面信息进行建模，然后使用与建模方法对应的算法或工具，验证对应模型下的策略不变式，以检测出不符合策略的错误，保证网络的真实行为与该策略一致。


 

在SDN中，网络行为是集中由控制器决定的，这使得验证网络变得简单。目前SDN控制平面验证主要集中在两方面，一是对SDN程序的验证，二是开发验证控制器[3]。SDN使用应用程序制定策略管理网络设备，如路由或访问控制。如普通的软件程序一样，SDN程序会出现设计或实现错误，如果盲目的部署在网络中，很容易引起故障的发生。验证控制器用于检查控制器是否按照策略正确安装规则，因为其特定的编程语言支持不变式验证，可以在编译时与规则安装到交换机之前进行验证，防止错误的规则下发。目前，SDN程序验证方向有Verificare、VeriCon等工具，验证控制器方向有NetCore、NDLog、NetKAT等工具。

数据平面验证

数据平面验证通过输入数据平面信息，验证网络策略的不变式以确保数据平面与策略要求的一致。其优点是数据平面直接体现了配置的影响，分析起来更加简单。但是，其不能在配置部署前完成验证，而且需要重复采集数据以应对网络波动带来的数据平面变化。此外，数据平面验证不能提供错误配置的出处，需要人员自行关联发现，由于网络行为与配置文件之间的复杂关系，这是十分困难的。数据平面验证方面，传统网络与SDN网络的唯一区别在于数据采集过程，传统网络可以通过SNMP(简单网络管理协议)，终端或者控制会话来收集转发表，而SDN网络可以监视控制器获得。

由于控制平面验证不能发现网络设备将控制平面转换成数据平面的实现错误，以及存在分析复杂的问题，Mai等人于2011年提出了第一个在真实网络中发现错误的数据平面分析工具Anteater[10]。Anteater首先根据数据平面信息将网络建模成为一个图，然后将不变式建模为图上的函数，最后将函数转换为SAT公式放入SAT Solver进行求解。Anteater通过实验证明，分析数据平面是一种可行方法，相比于控制平面验证速度不一定更快，但实现方法上相比更容易。

Kazemian等人之后提出了一种数据平面验证框架HSA [11]。HSA框架是基于几何模型的，其将数据包建模成几何空间中的点，用头空间(Header Space)即最大长度为L的{0,1}字符串表示，网络设备建模成该几何空间上的转移函数，通过分析特定数据包头部在几何空间的变化，进行不变式的验证。相比于其他基于形式化验证方法的工具，HSA可以提供所有反例，使分析错误变得高效。Veriflow和NetPlumber使用等价类与增量技术分别改进了Anteater和HSA，有足够的速度和扩展性。

Lopes等人认为，Veriflow和NetPlumber是定制化的代码，难以扩展到新的数据包格式和协议。而网络验证若要发展成为一个网络CAD行业，必须要发展成一个更标准化、更加可扩展的技术。为解决该挑战，Lopes等人基于Datalog技术，提出了NOD工具[12,13]。NOD使用Datalog对策略和协议行为编码，能够进行通用的扩展，最后使用基于SMT Solver技术的Z3 Datalog框架进行验证。实验表明，NOD的Datalog模型计算可达数据集合比模型检测和SMT计算单个可达数据都快，相比于基于HSA的Hassel工具，虽然速度相比较慢，但更易于通用化。为专注于验证访问控制策略的正确实施，Jayaraman等人提出了SecGuru工具，是NOD的早期版本, 已经被部署在Azure中以检查数以百计的路由器和防火墙的正确性[14]。

SecGuru使用位向量对数据平面和策略进行编码，然后将这种位向量逻辑放入Z3 SMT Solver完成验证。表2从表达性、扩展性、主要基于的技术3个方面对上述工具进行了总结，其中，表达性是指分析网络功能的能力，如路由、NAT(网络地址转换)、IP分片等，扩展性是指工具扩展到大型网络的能力。

 

Batfish并没有选择在控制平面上进行建模，而是选择通过控制平面生成数据平面，然后调用数据平面验证工具进行验证。这种方式结合了控制平面验证和数据平面验证的优点，既能提前检测错误也不需考虑协议的复杂交互。但是，Batfish面临着一个难题，即如何根据配置和环境生成一个可靠的数据平面，其通过使用DataLog(一种数据查询语言)的一种变式LogiQL建立了一个陈述式模型以解决此挑战。由于Batfish需要对整个数据平面进行模拟，速度很慢。Gemberjacobson等人发现，生成详细的数据平面是不必要的，提出了ARC，可以直接在控制平面进行快速分析[7]。

ARC使用加权有向图对控制平面建模，使用图算法进行分析完成验证。对于特定的属性不变式，可以比Batfish快出了三个数量级。但是，ARC只对一些特定的协议组合进行了分析，如OSPF，RIP，eBGP。为提高验证的协议范围，Fayaz等人提出了ERA工具[8]。

ERA使用二元决策图(BDD)对控制平面建模，通过探索BDD模型完成验证。相比ARC可以验证更多协议，相比Batfish验证速度快了2.5到17倍，且可以扩展到大型网络中。Beckett等人指出，控制平面验证的主要难点在于构建一个具有高度的网络设计覆盖范围与高度数据平面覆盖范围的验证工具，同时保持足够高的可扩展性[9]。

其中，网络设计覆盖范围是指工具能够支持网络的拓扑类型、路由协议和其他一些特点的范围;数据平面覆盖范围是指工具能够支持的数据平面的范围。为解决该挑战，Beckett等人提出了Minesweeper工具。Minesweeper使用SMT公式对控制平面建模，将公式放入SMT Solver中完成验证。相比之前的控制平面验证工具，可以验证更多的协议，覆盖更大的数据平面，且可以扩展到大型网络。值得说明的是，ARC、ERA和Minesweeper都使用了Batfish的配置解析器将不同厂商的配置转换为无关厂商的统一格式。表1从网络设计覆盖范围、扩展性、主要基于的技术3个方面对上述工具进行了总结。其中，扩展性是指工具扩展到大型网络的能力。

（编辑：济南站长网）

【声明】本站内容均来自网络，其相关言论仅代表作者个人观点，不代表本站立场。若无意侵犯到您的权利，请及时与联系站长删除相关内容!