简介随着网络变得复杂和庞大，网络管理变得更加困难，网络升级或改造过程中的小失误都可能影响网络的正常运行。网络。造成严重影响。根据Veriflow2016年对315名IT专业人员的调查结果，59%的受访者表示网络复杂性的增加导致更频繁的中断，74%的受访者表示每年或多次发生网络变更对企业产生重大影响[1].2019年7月3日，Cloudflare在新的Web应用层防火墙中部署了配置错误的规则，导致全球中断[2]。配置错误、硬件和软件实施错误、网络攻击或协议交互中的意外错误都会影响网络的可用性和安全性。那么关键的问题是，在复杂的网络环境下，如何保证业务意图的正确实现？在过去的几年中，出现了一个新的研究领域，即网络验证，其目的是严格确保网络按照预期的业务意图运行。跑步。网络验证的技术灵感来源于形式化方法，形式化方法是广义上建立在数学方法之上的。通过为复杂系统建立严格的数学模型，验证系统性能和行为正确性的方法主要包括模型检验、定理证明和符号执行。以及SMT/SAT（可满足性理论）求解器四种技术[3]。形式化验证已成功应用于硬件和软件领域。例如，NASA（美国国家航空航天局）成功地使用形式验证技术发现了火星探测器飞行软件中的并发错误[4]。如果我们可以验证硬件和软件，为什么不验证网络呢？最近，网络验证在验证和编程语言社区中开始流行，学术界和工业界都开展了网络验证的研究。在学术界，主要有斯坦福大学、伊利诺伊大学香槟分校、加州大学洛杉矶分校、卡耐基梅隆大学、清华大学等大学。业内主要有微软研究院和AT&T实验室。目前，该领域已经涌现出一些初创公司，如ForwardNetworks、Veriflow、Intentionet等。本文将首先介绍一些相关的背景知识，然后介绍网络验证中控制平面验证和数据平面验证这两个研究方向，最后进行总结。背景知识网络从路由和转发的角度可以分为三层，即策略、控制平面和数据平面，如图1所示[3]。策略是控制平面和数据平面的参照，反映了网络管理员的意图，例如是否允许主机A与主机B进行通信。控制平面用于执行策略。在传统网络中，指的是分散在各处的网络设备中的配置文件。在SDN（SoftwareDefinedNetworking）中，指的是各种应用。数据平面是网络中控制平面生成的转发信息和拓扑结构。转发信息是指传统网络中的转发表和SDN中的流表。根据控制平面和数据平面两个层次，网络验证有两个研究方向：控制平面验证和数据平面验证。它通过分析相应的平面信息来完成检查，然后验证网络策略的不变性。其中，不变量是一个属性，具体指网络中路由转发行为的正确属性，如无转发环路不变量，断言数据包在网络中不会有转发环路。在验证企业网或校园网等特定网络时，除了网络的控制平面或数据平面信息外，网络环境的因素，如从网络外部发送到网络的路由通告，被考虑。图1NetworkHierarchyDivisionControlPlaneVerification控制平面验证通过输入控制平面信息来验证网络策略的不变性，确保控制平面与策略要求一致。其优点是可以在配置部署到网络之前完成验证，可以轻松定位错误的配置位置；缺点是需要分析配置文件与网络行为的复杂关系，需要考虑各种配置语言。目前传统网络仍占据主导地位，其控制面的配置文件分散在各处的网络设备中，验证面临状态爆炸的问题。在相关研究方面，Feamster等人。2005年提出rcc工具[5]，这是第一个能够检测真实网络BGP（BorderGatewayProtocol）故障的静态分析工具，但其检测范围仅限于BGP协议。rcc采用静态分析的方式，将控制面信息标准化为SQL数据，然后根据policy转换的SQL上的约束条件来验证BGP配置的正确性。为了提高验证范围，不再局限于特定的协议，Fogel等人。提出了Batfish工具[6]。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倍，可以扩展到大型网络。贝克特等人。指出控制平面验证的主要难点是构建一个具有高网络设计覆盖率和高数据平面覆盖率的验证工具，同时保持足够高的可扩展性[9]。其中，网络设计覆盖率是指工具能够支持网络的拓扑类型、路由协议和其他一些特性的范围；数据平面覆盖是指工具可以支持的数据平面范围。为了应对这一挑战，贝克特等人。提出了扫雷工具。Minesweeper使用SMT公式对控制面进行建模，并将公式放入SMTSolver中完成验证。与以往的控制平面验证工具相比，它可以验证更多的协议，覆盖更大的数据平面，可以扩展到大型网络。值得注意的是，ARC、ERA、Minesweeper都使用Batfish的配置解析器，将不同厂商的配置转换成统一的格式，不分厂商。表1从三个方面总结了上述工具：网络设计覆盖率、可扩展性和主要基于的技术。其中，可扩展性是指工具扩展到大型网络的能力。表1传统网络控制平面验证工具总结在SDN中，网络行为由控制器集中决定，这使得验证网络变得容易。目前SDN控制平面验证主要集中在两个方面，一是SDN程序的验证，二是控制器的开发和验证[3]。SDN使用应用程序制定策略来管理网络设备，例如路由或访问控制。与普通软件程序一样，SDN程序可能存在设计或实现上的错误，如果盲目部署在网络中，很容易导致故障。验证控制器用于检查控制器是否根据策略正确安装规则，因为其特定的编程语言支持不变验证，可以在编译期间和规则安装到交换机之前进行验证，以防止错误的规则传递。目前，SDN程序验证有Verificare、VeriCon等工具，控制器验证有NetCore、NDLog、NetKAT等工具。数据平面验证数据平面验证通过输入数据平面信息来验证网络策略的不变性，确保数据平面与策略要求一致。好处是数据平面直接反映了配置的影响，分析起来更容易。但配置部署前无法验证，需要反复采集数据，以应对网络波动带来的数据平面变化。此外，数据平面验证无法为错误配置提供来源，需要人工关联才能发现它们，由于网络行为和配置文件之间的复杂关系，这很困难。在数据平面验证方面，传统网络与SDN网络的唯一区别在于数据采集过程。传统网络可以通过SNMP（简单网络管理协议）、终端或控制会话收集转发表，而SDN网络可以通过监控控制器获取。由于控制平面验证无法发现网络设备将控制平面转换为数据平面的实现错误，并且存在复杂的分析问题，Mai等人。2011年提出第一个数据平面分析工具Anteater，用于发现真实网络中的错误[10]。Anteater首先根据数据平面信息将网络建模成图，然后在图上将不变量建模成函数，最后将函数转化为SAT公式，放入SATSolver求解。Anteater通过实验证明，分析数据平面是一种可行的方法。与控制平面相比，验证速度不一定更快，但实现方法更容易。卡泽米安等人。后来提出了数据平面认证框架HSA[11]。HSA框架基于几何模型，将数据包建模为几何空间中的一个点，在头部空间（HeaderSpace）中用一个最大长度为L的{0,1}字符串表示，网络设备被建模为几何空间传递函数，通过分析特定包头在几何空间中的变化来验证不变量。与其他基于形式化验证方法的工具相比，HSA可以提供所有反例，使得分析错误变得高效。Veriflow和NetPlumber分别使用等价类和增量技术改进了Anteater和HSA，具有足够的速度和可扩展性。Lopes等人认为Veriflow和NetPlumber是定制代码，很难扩展到新的数据包格式和协议。但是，如果网络验证要发展成为网络CAD行业，就必须发展成为一种更加标准化和可扩展的技术。为了解决这一挑战，Lopes等人。提出了基于Datalog技术的NOD工具[12,13]。NOD使用Datalog对策略和协议行为进行编码，可以进行通用扩展，最后使用基于SMTSolver技术的Z3Datalog框架进行验证。实验表明，NOD的Datalog模型计算可达数据集比模型检查和SMT计算单个可达数据更快。与基于HSA的Hassel工具相比，虽然速度相对较慢，但更容易泛化。为了专注于验证访问控制策略的正确实施，Jayaraman等人。提出了NOD的早期版本SecGuru工具，该工具已部署在Azure中以检查数百个路由器和防火墙的正确性[14]。SecGuru使用位向量对数据平面和策略进行编码，然后将这个位向量逻辑放入Z3SMTSolver中完成验证。表2从三个方面总结了上述工具：表现力、可扩展性和主要基于的技术。其中，表达性是指分析网络功能的能力，如路由、NAT（网络地址转换）、IP分片等。可扩展性是指工具扩展到大型网络的能力。表2数据平面验证工具总结总结网络验证的目的是确保网络忠实地按照高层的策略意图运行，即网络的真实行为与策略一致。本文主要对网络验证中控制平面验证和数据平面验证两个方向的现有研究进行简要概述。整体来看，大部分工具都是基于形式化方法实现的，例如基于SMT/SAT求解器的Minesweeper、Batfish、Anteater、NOD、SecGuru；基于符号执行的HSA。rcc、ARC、ERA等其他工具通过不同的建模方式实现验证。上述工具的特点是基于模型的形式化验证，本质上是一种状态机验证技术。其总体框架如图2所示，首先对平面信息进行建模，然后使用建模方法对应的算法或工具验证相应模型下的策略不变性，检测不符合策略的错误和确保网络的真实行为与该策略一致。图2控制平面验证和数据平面验证的总体框架除了控制平面验证和数据平面验证，网络验证还有很多其他的方向。例如，网络测试通过生成测试包，确保网络设备按照控制平面忠实地建立转发信息，并按照转发信息忠实地完成转发；网络规范的自动综合旨在开发一个综合工具来自动生成正确的配置；NetworkDebugging旨在找到网络域中逐步调试、监控、断点、挂起或恢复等功能的等效实现。未来网络验证还需要解决一些问题，比如有状态网络下的验证（比如包含有状态防火墙等中间件的网络）、复杂路由场景下的控制面验证、常量属性（时延、带宽）类型验证，ETC。参考文献[1]Veriflow。网络复杂性、变化和人为因素正在使业务失败。https://www.veriflow.net/survey/.[2]约翰·格雷厄姆-卡明。错误的软件部署导致Cloudflare中断[EB/OL]。https://blog.cloudflare.com/cloudflare-outage/,2019-07-02.[3]LiY,YinX,WangZ,etal.形式化方法网络验证与测试综述：途径与挑战[J]．IEEECommunicationsSurveysandTutorials,2019,21(1):940-969.[4]BratG、DrusinskyD、GiannakopoulouD等人。火星探测器软件验证与验证工具的实验评估[J].系统设计中的形式化方法,2004,25(2-3):167-198.[5]FeamsterN,BalakrishnanH.使用静态分析检测BGP配置错误[C]。网络系统设计与实现，2005：43-56.[6]FogelA、FungS、PedrosaL等人。网络配置分析的一般方法[C]．网络系统设计与实现上,2015:469-483.[7]GemberjacobsonA、ViswanathanR、AkellaA等人。使用抽象表示的快速控制平面分析[C]。acm数据通信特别兴趣小组，2016：300-313.[8]FayazSK、SharmaT、FogelA等人。使用简洁的控制平面表示的高效网络可达性分析[C]。操作系统设计与实现，2016：217-232.[9]BeckettR、GuptaA、MahajanR等人。一种网络配置验证的通用方法[C]．acm数据通信特别兴趣小组，2017：155-168.[10]MaiH、KhurshidA、AgarwalR等人。用anteater调试数据平面[C].acm数据通信兴趣小组,2011,41(4):290-301.[11]KazemianP、VargheseG、MckeownN等人。头部空间分析：网络静态检查[C].网络系统设计与实现，2012：9-9[12]LopesNP,BjornerN,GodefroidP,etal.检查动态神经网络中的信念作品[C].网络系统设计与实现，2015：499-512.[13]LopesNP、Bj?rnerN、GodefroidP等人。基于程序验证的网络验证[J].MSR，代表，2013.[14]JayaramanK、Bj?rnerN、OuthredG等人。网络连接策略的自动化分析与调试[J].微软研究院，2014年：1-11。
