转载请注明出处，本人能力有限，有不足、不对之处欢迎各位讨论。全部图已经省略。

配置综合与验证学术研究洞察报告

1.1 配置综合

网络配置综合是自动驾驶网络架构下的关键技术之一。人工配置存在的效率低、故障率高的问题，配置综合技术致力于实现配置生成与配置更新的自动化处理，用综合计算的方式代替人工配置过程。配置综合从应用的角度可以分为绿地配置综合与棕地配置综合，相关论文也多会偏重于其中一个方向。

（a）绿地配置综合

绿地配置综合通过输入配置策略与网络拓扑，在空白的网络中综合生成满足策略的配置。其中配置策略描述的描述方法多使用DSL技术，后续的求解计算过程根据策略转换的约束格式及协议配置特点多使用SMT（MaxSMT）和图方法进行求解。

早期的配置综合用于解决SND网络控制器中OpenFlow协议配置操作复杂的问题。Frenetic通过引入一系列用于查询和转换网络流的组合运算符，实现了高级别的网络查询和网络策略管理库[1]。Frenetic简化了对OpenFlow控制器的部分操作，但只能被动实现网络策略管理，而无法主动地通过描述网络策略来实现配置综合。然后NetKAT在Frenetic的基础上，结合正则表达式和有限状态自动机来对数据包的网络路径进行表达，使用KA (kleene代数)对正则表达进行处理[2]。NetKAT提高了网络配置的描述程度，因此可以使用更少的NetKAT语言描述庞大底层网络配置，并且保证了配置的正确性。接下来的Genesis是通用多租户数据中心网络的配置综合系统[3]。管理员通过声明式语言指定网络策略，不需要需显式地对网络数据平面进行编程。Genesis使用了分而治之的综合程序，利用隔离策略之间的依赖关系来提高综合性能。 该过程将输入策略划分为多个组件，以便Genesis可以分别合成组件来加快合成完整问题速度。Genesis将约束求解的形式化推理和SMT约束求解器结合，将高层策略自动生成数据平面配置，解决编程与配置交换机的困难。从扩展性来看，Genesis存在局限性，仅支持集中式的数据中心网络，只支持静态路由配置。后期随着技术的累积和OpenFlow的局限性，配置综合技术逐渐将研究重心转移到传统网络中。

在传统网络中的配置综合研究大致可以分为两类。一类偏重于“策略”到“约束”的求解过程。Propane是实现BGP协议的流量路径策略的配置综合系统[4]。Propane用DSL来表达路由器BGP协议的几种常用策略和网络拓扑结构。使用正则表达式和有限状态自动机来表达流量的传输路径。计算每个IP前缀的可能路径和最优路径，并以此为路由器设置优先级。Propane具有容错检验的功能，可以对将要生成的配置进行验证，避免产生错误，如出现路由黑洞。Propane/AT在Propane的基础上提出了抽象拓扑图的概念[5]。抽象拓扑把实体拓扑中作用相似的一个或多个实体节点抽象为一个角色节点。通过这种方式缩小了求解过程中使用到的拓扑规模，提高了生成配置的复用性。另一类偏重于“约束”到“参数”的求解过程。Synet是基于多种路由协议的配置生成系统，支持OSPF、BGP、静态路由协议[6]。Synet采用形式化推理的方法，将配置求解问题转化为求解Datalog问题的输入问题，在层次迭代中使用SMT求解。但Datalog问题缺少灵活性，不因网络拓扑和需求的改变而改变。Synet使用Datalog简化了网络配置，但在Datalog问题转化为SMT约束求解时，搜索空间过大导致求解速度不理想。Netcomplete将配置生成问题简化为用SMT求解器求解的约束满足问题，在SMT约束求解基础上，增加了Configuration sketch、BGP sketch和反例引导归纳合成（Counter-Example Guided Inductive Synthesis）算法加速求解，基于符号化的标准配置模板来求解关键参数，最终生成满足策略的配置文件[7]。当前致力于P4网络配置综合（P4代码自动生成）的研究颇少，发表在NSDI2020的Contra是这个领域近期的研究工作[8]。其借鉴了传统网络配置综合工作Propane的思想，通过结合网络拓扑，分析用户编写的全网策略，生成本地交换机P4程序。P4程序逻辑则是借鉴了数据平面的一项研究工作HULA，其实现了自定义的距离矢量协议，该协议生成探针遍历网络，收集路径利用率等信息，交换机根据这些信息决定数据包转发的下一跳。

（b）综地配置综合

棕地配置综合指在已存在配置的网络中根据更新需求对配置进行更新操作。通常输入为配置文件和更新策略，输出为更新操作或更新后配置。现有的研究多使用形式化求解的方法进行棕地配置综合。

SDN网络中棕地配置综合研究较少，NetGen是对现有网络状态或策略进行变更的DSL，使用了SMT求解技术[9]。它以当前网络状态和变更策略作为输入，使用基于抽象和约束求解的模型计算出满足条件的最佳变化策略。NetGen将数据包抽象，并为其创建网络模型，使用z3求解器求解出所有满足约束条件的数据平面配置。

在传统网络中，Jingjing使用DSL语言LAI实现了ACL配置的自动更新需求，实现了基于意图的网络ACL更新配置，综合运用了配置综合技术和配置更新验证技术，为配置综合方法的研究提供了新的解决思路[10]。AED将配置更新过程自动化，建模为语法树添加和删除的集合。AED将当前配置以及网络策略需求编码为SMT约束，将管理目标(保持网络设备之间的结构相似性、尽可能减小网络设备配置参数的修改)编码为软约束，即最大限度满足这些软约束[11]。通过Z3 MaxSMT 求解器求解关键参数，得到更新后的配置文件。Snowcap提出一种满足软约束硬约束的综合框架，将配置更新问题表述为约束条件下的优化问题，将初始配置和目标生成的配置解析，采用反例引导搜索来优化查找最优的重新配置顺序[12]。

（c）配置综合相关研究展望

（1）配置意图表示与转译

配置意图的表示与转译是配置综合的一个关键研究点，现有配置综合方法的配置意图表示与转译存在策略描述范围小、语法差别大及抽象程度不同的问题。我们计划将配置意图表示与转译进行单独研究，尝试将自然语言作为配置意图的载体，实现“配置意图”到“约束”的转译过程。

配置意图以一种声明的形式描述用户想要网络所达到的状态，而不用描述如何实现意图，用户意图的表达形式有很多，最普遍的是自然语言的形式，此外还有用户的语音输入或者相关的GUI输入等。在网络领域，根据意图抽象级别的高低，意图的表示可以分为完全无约束的自然语言、有约束的有限自然语言、针对特定领域的领域特定语言（DSL，Domain Specific Language）以及最为具体化的设备配置文件。而意图的转译过程则是指根据意图中的内容以及当前网络状态将用户意图转化为相应的网络配置策略。在基于意图的网络中意图的获取和转译是关键性的工作。

意图的转译过程是根据意图中的内容以及当前的网络状态将用户或管理员的意图转化为相应的网络配置策略。目前，用户意图的转译主要采用自然语言处理的方法对意图进行处理，对用户意图进行关键字提取、词法分析、语义挖掘等操作，从而获得用户期望的网络运行状态，并使用智能化的方法生成网络策略。iNDIRA系统利用自然语言处理和本体论的方法在SDN控制平面和应用之间实现了意图转译模块，用户以自然语言的形式输入意图，该模块将自然语言处理为RDF图，并自动生成网络策略或配置命令，从而实现意图的转译，该方法为意图的转译工作提供了指导性的方案[13]。Liao等人提出了基于模板的策略生成方法，系统预先定义网络策略库,将不同类型的网络策略存储在策略库中，当用户意图输入时，即可使用自然语言处理的方法获取关键信息，并根据策略库映射为相应的网络策略[14]。另外，Riftadi 等人创建了一个 P4 的代码模板库，将用户意图映射为P4代码[15]。Beigi等人提出了基于案例学习的方法，通过用户意图的不断输入，系统将不断学习意图的特征，并生成相应的策略[16]。Jacobs等人提出了一种新颖的意图简化过程，使用机器学习从自然语言智能提取意图，再使用来自网络运营商的反馈来改善学习，同时还提出了一种类似于英语的高级、全面的意图定义语言Nile[17]。用于充当其它策略机制的抽象层，减少了运营商为各种不同类型的网络学习新的策略语言的需要。

针对自然语言到领域特定语言的转译方面的研究也是业界研究的热点。其中，NL2SQL（Natural Language to SQL）就是其中之一。NL2SQL的本质是将自然语言转化为计算机可以理解并执行的规范语义表示。Zhong等人最先提出了深层神经网络Seq2SQL，使用在数据库中循环查询执行的奖励来学习生成查询的策略，该策略包含不太适合通过交叉熵损失进行优化的无序部分[18]。此外，利用SQL的结构来修剪生成查询的空间，并大大简化生成问题。除了这个模型之外，还发布了WiKiSQL，一个大型标注NL2SQL数据集，也是目前规模最大的NL2SQL数据集。Hwang等人探索了基于BERT体系结构的三种变体，其最佳模型在逻辑形式和执行精度方面分别比以前的先进技术高出8.2％和2.5％，该分数接近WikiSQL的上限，并观察到大多数评估错误是由于错误的标注引起的，除此之外其模型准确性超过了人类，执行精度上提升至少1.4％。自NL2SQL提出后，几年来业界又提出多种模型，从最开始简单的Seq2Seq模型，逐渐发展到多任务、迁移学习、以及基于BERT和MT-DNN预训练的模型，准确率也从最开始的不足四成提升至目前的超过九成[19]。

意图的转译方法主要根据意图表示的抽象级别不同而有所区别。当前针对自然语言到网络策略的转译方法，以输入关键词以匹配先前编写好的网络策略库为主。近年来，机器学习、深度学习等新兴概念兴起，各种互联网新技术层出不穷，在自然语言翻译领域，随着卷积神经网络、循环神经网络的提出与发展，端到端的机器翻译也从最早的基于词典和语法生成的也就是基于规则的机器翻译发展到如今的基于神经网络的机器翻译。近年来针对自然语言到领域特定语言的转译工作由于网络配置领域的意图表示数据有限而难以取得突破，建立网络配置领域的统一表示形式是要解决的关键科学问题。另外，网络配置必须是确定的、无误的，而采用深度学习、深度神经网络方式进行的翻译效果还有待检验和提高。对于意图的转译工作，不同的方法有各自的优缺点，缺少一个较为完善的解决方案。此外，对于用户意图的分析也是一个亟待解决的问题，目前的研究往往局限于一些简单的、特定环境下的意图描述或者策略描述，这使得一些研究工作往往忽略了意图的分析工作。意图的分析工作主要使用自然语言处理的方法，但是目前自然语言处理方法对于语义挖掘等任务的处理能力有限，因此要想完美实现意图的转译工作，对于意图的语义挖掘等问题还需要进一步的研究与探索。

（2）配置翻译

在当今社会中，网络成为不可或缺的一部分，而交换机、路由器等设备在网络起到了至关重要的作用。当设备发生硬件故障，或园区进行整体搬迁时，可能会维持之前的网拖拓扑结构，但把原设备更换为其他型号的新设备，这种更新可能发生在同一厂商的不同型号之间，也可能发生在不同厂商的不同型号之间。为了维持原有功能不发生变化，需要把原有的配置文件翻译为新型号设备对应的配置文件，满足新型号设备的语法以及规范。

当前完成此工作的主要方式之一是专家逐个挑选原型号和新型号的对应语句，在数据库中保存，再由机器逐语句地进行配置文件的翻译。此方法消耗了大量人力，并且每当出现新型号的设备时，都需要专家再次匹配语句，几乎不存在拓展性。

网络配置翻译目前是一个研究较少的领域，与之相关的公开论文研究基本没有。目前能找到的关于网络配置翻译的工具只有工业界各家公司的产品，以相关文档中提到的华为 eDesk 工具为例，其中配置翻译部分的主要功能是将思科以及华为相关设备的配置文件转化为华为设备配置文件，用于提高华为自家网络设备的可用性和兼容性。并且这款工具仅支持转换成华为的配置，不支持双向的转换，并且支持的设备有限，对新设备的支持度较差，虽然有一定的扩展性支持添加配置但是不开放源码，同时需要购买华为的设备才能使用。

此外，2002 年 Dominic Chorafaki 等人发明的一个网络设备间配置文件的翻译的专利中介绍了一种简化命令行接口配置脚本翻译的系统和方法[20]。该系统包括一个翻译器以及一个或多个数据字典。每一数据字典包括以多种CLI 脚本类型为依据所产生的共同句法。翻译器对来自与原设备相关的脚本进行自动翻译，并将其翻译到具有不同脚本要求的设备中。不过相关文件没有提供具体实现的程序或软件，而且专利只是简单介绍了流程，没有详细说明其算法的实现，并且由于这份专利发布较早，与当前的主流网络配置并不完全贴合，参考价值有限。由于该领域研究较少，故从课题组现有研究出发，拟采用以下技术实现配置翻译。

1. 知识图谱

“知识图谱”一词在提出之处特指 Google 公司为了支撑其语义搜索而建立的知识库。随着知识图谱技术应用的深化，知识图谱已经成为大数据时代最重要的知识表示形式。作为一种知识表示形式，知识图谱是一种大规模语义网络，包含实体、概念及其之间的各种语义关系。通过华为设备的产品文档，构造网络配置领域的知识图谱，实现网络配置领域的知识表示，使不同型号设备的配置语句能够通过此知识图谱构建起联系，并通过对知识图谱的查询等操作实现不同设备的语句的对应。

2. 自然语言处理

知识图谱的构建过程离不开自然语言处理，从词汇挖掘与实体识别到关系抽取，都需要通过自然语言处理实现。在网络配置领域的知识图谱构建过程中，由于几乎没有已经标注过的数据，所以采用半监督或者无监督的自然语言处理方法。

3. 句法树

通过对产品文档的学习，可以建立一棵句法树,与AED中的句法树相似，用来表示语句所在的视图，以及语句的顺序关系，使翻译后的语句能够在正确的位置上，保证语句顺序的正确性。在句法树中，根节点为系统视图，并无具体语句。对于其他节点，其父节点是进入所属视图的语句。

4. 父视图信息栈

在翻译的过程中可能出现原设备的多条语句共同翻译为新设备的一条语句的情况，我们假设出现这种情况时原设备的多条语句一定在一系列相互包含的视图下，且翻译时必须包含的信息不会只能从其他视图获取。在这样的假设下，通过建立父视图信息栈可以解决“多对一”翻译的问题。每当进入一个新的视图，把此语句的信息压栈，退出视图时根据退出视图的层数决定弹栈的次数，如此便可保存相关信息。

（3）P4网络配置综合

传统上，数据平面被设计成具有固定的功能，使用一组协议来转发数据包，这种封闭的设计模式限制了交换机的能力，导致整个网络构建过程冗长、昂贵、不灵活。最近，数据平面的可编程性引起了研究界和工业界的极大关注，其允许管理员和程序员运行自定义的包处理功能。这种开放的设计模式为将来的创新和实验开辟了道路，减少了协议的设计、测试到最后使用的时间，使程序员能采用自定义的、自顶向下的方法开发网络应用程序，降低了可编程交换机的复杂性，提高了卸载到数据平面的应用程序的性能。

P4是当前可编程数据平面的主流高级编程语言。使用P4语言编写网络内应用并非易事。最近的研究表明，许多现有的P4程序存在一些可能导致网络中断的bug。几十年来，网络行业一直以自底向上的方式运作，其中交换机配备了固定功能的ASICs。因此，网络运营商几乎不需要编程技能。而可编程交换机的出现要求操作人员具有ASIC编程经验。同时随着大数据、云计算等产业的兴起，各大互联网公司都在大力建设数据中心，其网络规模及其庞大，为这些设备编写P4程序的工作量更是超乎想象，而且由于ASIC的编程不是一项简单的任务，故研究工作应该考虑简化操作人员的编程工作。在传统网络中，为了提高配置效率，降低配置出错概率，配置综合理论与方法应然而生。受到配置综合理论与方法的启发，我们完全可以提出用于可编程数据平面的P4综合理论与方法，来解决上述问题。

对于P4网络下的配置综合，存在以下四方面关键问题需要解决。

1.   自定义协议的设计问题

由于P4具有协议无关的特性，这为P4综合提出了第一个严峻的问题，要想在网络中实现特定的功能（如三层转发），首先需要设计一个协议，包括数据包头的格式等。

2.   用户意图DSL的设计问题

和传统网络配置综合思想一致，P4综合同样需要设计能够使用户表达网络策略的DSL，同时，P4综合系统还需要具备意图理解与解析的功能。

3.   P4综合求解效率问题

随着网络规模的不断变大，设备越来越多，求解效率也是必须考虑的一个问题。研究高效、可扩展的P4综合方法，提升P4综合求解效率是至关重要的。

4.   P4更新与验证问题

网路动态性强、需求变化频繁；即使是自动生成的P4代码，也不能保证完全正确，部署之后很有可能导致网络故障。因此研究P4代码更新与验证方法是关键的一个问题。

围绕以上问题，结合现有研究，课题组计划以数据平面ACL作为研究目标，研究在P4网络下的ACL的配置综合方法。

（4）SRv6配置综合

SR技术通过控制平面分发标签，在数据平面仍然基于MPLS转发。随着IPv4向IPv6演进，为实现在IPv6数据平面实现转发，通过网络编程实现业务和承载的结合，避免业务与承载分离带来多种协议互联互通问题，灵活提供服务。5G改变了连接的属性，在5G的应用场景下，网络业务需求各异，例如更强的SLA保证、低时延，增加连接的属性，需要报文携带更多的信息，5G承载网通过引入SRv6技术满足这些要求。

SRv6是基于IPv6的分段路由技术，分段路由技术需要为网络中的每个节点和链路分配Segment,头节点把Segment组合起来形成Segment序列，指引报文按照Segment序列进行转发来实现网络编程能力。SRv6利用IPv6 128 bit地址的可编程能力，丰富了SRv6指令表达的网络功能，可标识转发路径的指令，SRv6有强大的扩展能力，如果要部署一个新的网络功能，只需要定义一个新的指令即可，不需要改变协议的机制或部署。SRv6 Policy实现业务的端到端需求，是实现SRv6网络编程的主要机制。配置SRv6

Policy时，必须配置Endpoint、Color以及Candidate Path的Preference和Segment List，且不允许配置重复的Preference。SRv6所需的配置参数繁多，同时需要IGP、BGP扩展来支持SRv6的配置，协议之间存在依赖对配置工作提出新的要求，同时考虑到IPv6可达性，适用于跨域场景，因此拟研究基于意图的SRv6配置生成的方法。基于意图的SRv6配置自动生成方案整体流程为：对网络拓扑、和网络协议(SRv6、BGP、ISIS)进行形式化描述,经过解析，将需求描述转换成布尔逻辑表达式，每一个布尔表达式表示一个配置参数，找出满足所有布尔逻辑表达式为真的解，确定每个配置参数的值。对于SRv6协议形式化建模为M⊨Requirements⋀ProtocolSRv6、BGP、ISIS ⋀Policies，其中Requirements用来表示对业务流量的路径要求，Protocol表示确定的网络协议语义，用以定义路由器根据路由协议的哪些属性进行选路，Policies定义参数如何赋值使该布尔表达式为真。下面是对其步骤的展开。

首先设计意图语言用于表达网络策略来表示业务流量转发要求，然后使用形式化方法对各网络协议建模求解并提出相关生成算法。由于SRv6协议基于BGP、IGP(ISIS/OSPFv3)扩展实现，因此需要同时对BGP和IGP协议进行建模。对于SRv6协议，设计生成算法将用户策略需求转换为对应SRv6 TE Policy实现，计算满足用户策略的Candidate Path。当使用控制器设备时，通过BGP-LS等收集网络拓扑、TE信息以及SRv6信息，并根据业务需求集中计算路径，然后通过BGP扩展协议将SRv6 Policy下发到头节点。考虑到AS间流量与负载均衡，需要额外输出BGP与IGP的配置需求分别由BGP处理模块和IGP处理模块来计算对应参数。在BGP处理模块中，设计生成算法生成符合BGP需求的配置，BGP通过修改路由通告属性来实现BGP路由控制和最佳路由选择，算法使用形式化方法对这一过程建模并求解关键参数，同时输出IGP配置需求。在IGP处理模块，设计生成算法生成符合IGP需求的配置，使用形式化方法对IGP计算最短路径的过程建模并求解关键参数，最后结合配置模板生成符合策略的配置文件。

接下来将带有管理目标的网络配置自动更新功能加入到网络配置综合,使得网络配置管理更加灵活实用，如2020年CoNEXT 的 AED，以及2021 SIGCOMM的Snowcap。对实际运行的网络添加网络策略后，用配置综合技术计算出目标配置参数，用更新模块计算出最优的配置顺序在真实运行的网络中进行添加。但是可能出现真实网络的配置无法直接过渡到目标配置，需要进行重新配置。因此在当前配置过渡到目标配置的过程中找到临时配置满足网络互通的要求是下一步研究的目标。

1.2 配置验证

网络验证有控制平面验证和数据平面验证两个研究方向，其通过分析对应平面信息，验证网络策略的不变式完成检查。

（a）控制平面验证

控制平面验证通过输入控制平面信息，验证网络策略的不变式确保控制平面与策略要求的一致性。其优点是可以在配置部署到网络之前完成验证，能够方便的定位到错误的配置位置；缺点是需要分析配置文件与网络行为之间的复杂关系，以及考虑形式各异的配置语言。

Batfish工具可以把形式各异的配置语言转换为无关厂商的统一格式[21]。Batfish并没有选择在控制平面上进行建模，而是选择通过控制平面生成数据平面，然后调用数据平面验证工具进行验证。这种方式结合了控制平面验证和数据平面验证的优点，既能提前检测错误也不需考虑协议的复杂交互。由于Batfish需要对整个数据平面进行模拟，速度很慢。目前Batfish的最新版本中，使用特定域算法来代替Datalog对控制平面进行分析。ARC提出生成详细的数据平面是不必要的，只需要相应的路径属性即可完成网络验证[22]。ARC采用有项加权图对控制平面建模，并采用图算法进行快速的分析和验证。但是ARC的验证范围(OSPF、RIP、eBGP)有限，无法满足大范围的验证需求。ERA采用二元决策图(BDD)对控制平面建模，通过探索BDD模型完成验证[23]。ERA能比ARC验证更多的协议，但它没有结合控制平面结构的全覆盖来分析一系列策略。Bagpipe采用反例搜索算法，并基于SMT进行求解，能够有效的在覆盖范围内(网络拓扑、协议等)对策略执行搜索验证[24]。但是Bagpipe只针对BGP协议进行了优化。为了验证更多的协议，覆盖更大范围的控制平面与数据平面，并可以扩展到大型网络中，研究人员提出了Minesweeper[25]。虽然Minesweeper能够实现良好的数据平面覆盖和功能覆盖，但在性能上付出了代价。且随着网络规模的增大，Minesweeper的扩展性很差，并且不能在合理时间内处理超过几百台设备的网络。为了进一步提升验证水平，以及支持更丰富的协议特征值。Plankton基于显式状态模型检查（ESMC），使用自定义语言对路由协议建模，这样的显式状态模型检查器可以探索由控制平面执行产生的许多可能的数据平面状态[26]。然而，ARC和Minesweeper都在性能和通用性之间做了艰难的权衡。Minesweeper和Plankton详细的编码使得验证性能变得非常差。除此之外，它们并不建模常见的网络特性，如VLAN。为了应对上述的问题，Tiramisu在基于ARC的基础上，采用一种新的、通用的多层图控制平面模型，可以为各种控制平面特性和网络设计构造建模[27]。这种编码允许Tiramisu为不同类别的策略使用不同的自定义验证算法，从而大大提高性能。其中有一点需要强调的是，ARC、RA、Minesweeper以及Tiramisu都使用Batfish将配置转换为无关厂商的统一格式。

ARC, ERA, Minesweeper以及Tiramisu都集中检查是否存在反例，例如违反某个属性(如陆航点)的固定失败场景，而不是计算存在多少反例以及它们发生的可能性有多大。也就是说，它们无法推断指定属性在网络处于给定状态时违反的概率。研究人员提出了概率配置分析器NetDice[28]。在给与网络配置额外的路由输入(可选)、概率故障模型和指定属性的情况下，NetDice可以准确的计算出指定的属性在网络处于给定状态时违反的概率。在不同的网络中，某些属性可以在指定的情况下被违反。因此，NetDice的概率计算结果有利于运营商对当前网络中服务水平协议的设计。然而，这些验证工具都有一个明显的限制，即必须由用户提供一个明确的、正式的网络预期行为规范(如可达性要求)。实际上，这种规范通常不完整或者不存在。需要注意的是，虽然Batfish不需要这种规范，但是它也仅限于识别一般配置错误(例如，转发循环，重复IP地址)，或者是独立于网络的特定策略意图。在网络中，由于担任同种路由角色的设备之间配置都高度相似或者基本相同，这为不需要网络规范而进行错误配置验证提供了可能性。SEFSTARTER是在没有规范的情况下通过离群点检测来推断可能的网络配置错误的方法[29]。给定一组配置元素，SEFSTARTER自动推断一组参数化模板，将人为的有意差异建模为模板内的变化，同时将非人为错误差异建模为模板间的变化。SEFSTARTER将配置进行分段，如分成BGP段或者ACL段。通过对不同段之间进行对比，自动推断可能的错误配置。对于这些配置验证工具，他们都应用在小型的网络中，例如小型供应商或者校园网。阿里巴巴在全球范围内部署了第一个实际的广域网配置验证工具Hoyan[30]，它支持在设备厂商行为不一致的情况下，不断发现设备行为模型中的缺陷，从而帮助操作人员修复模型。此外，这些配置验证工具也不适用于大型工业网络。虽然通过预先模拟的验证可以帮助发现配置错误，但是这种技术对于大型工业网络来说是昂贵的，甚至是非常棘手的。为了解决这一点，ShapeShifter使用抽象解释来解决这个问题，并发现正确的抽象可以降低网络模拟的渐近复杂性[31]。ShapeShifter准确的预测了95%网络的所有目的地的可达性，以及其余5%的大多数目的地的可达性。除此之外，ShapeShifter对网络控制平面的抽象解释不仅加快了现有分析的速度，而且有利于新类型的分析，并通过对BGP的分析来说明这一优势。虽然以上的配置验证工具对各种各样的问题进行了优化，例如协议范围，通用性，性能等。但是它们都没有对配置变更进行优化，也就是说他们不支持配置增量验证。为了解决配置的增量验证问题，RealConfig通过Differential Datalog增量计算配置更改，并输出数据平面的变更，最后在数据平面完成配置验证[32]。实验结果显示，RealConfig可以在1秒内验证配置更改。

（b）数据平面验证

数据平面验证通过输入数据平面信息，验证网络策略的不变式确保数据平面与策略要求的一致性。其优点是数据平面直观地体现了配置的影响，分析起来更加简单。

2011年发表的Anteater是第一个能够在真实网络中发现错误的数据平面验证工具, 验证包括IP转发表，ACL，VLAN标签等规则[33]。首先，它将获取的转发信息通过图模型建模成数据平面快照。其次，操作员定义了要针对网络进行检查的不变量（如转发，连通性，一致性等）并将其转换成图上的函数。最后将函数编码成SAT公式放入SAT求解器进行求解。一旦错误发生，Anteater会输出一个反例（如数据包报头或FIB条目）来帮助诊断。Anteater通过实验证明在数据平面进行分析是可行的，相比于控制平面验证不一定更快，但方法更加容易。然而，如果检测到策略违反情况，Anteater仅能提供一个反例，这很难确定导致冲突的转发规则。随后研究人员提出的验证工具HSA可以在策略违反时找到所有反例[34]。HSA是一个独立于供应商且与协议无关的验证框架，该框架基于几何模型，将数据包建模成几何空间中的点，将头空间用最大长度为L的0,1字符串表示。通过分析特定数据包头部在几何空间中的变化来验证不变量。它是一种将形式化方法（模型检查、符号模拟）与网络域特征相结合的新方法。HSA使用一些基于多维数据集压缩技术的优化来缓解状态空间爆炸问题，但是依然无法解决状态空间爆炸的问题。此外，Anteater与HSA等框架无法检测非直接网络冲突或执行状态监控。FLOVER扩展了这些技术，它是一个模型检查系统，能够验证Openflow网络下的流策略插入是否违反网络的安全策略[35]。

Anteater, HAS与FLOVER都是离线验证，如果FIB在收集过程中动态变化，将生成不一致的数据平面快照，从而导致误报；其次，如果网络出现可达性故障，则很难收集FIB快照；最后，这些系统具有较差的可扩展性且耗时都较长。VeriFlow[36]与NetPlumber[37]分别采用了等价类与增量技术改进了Anteater和HAS。其中，VeriFlow是第一个能在几百微妙内进行一次验证的数据平面验证工具，它对离线验证做出了突破。它将网络划分为等价类（ECs），每个EC表示具有相同转发行为的包。其次，它为每个EC构建单独的转发图。然后，它遍历这些图来检查不变量。当网络发生变化（例如插入转发规则）时，会影响极少数的ECs。但是，由于难以获得网络状态的完整视图，因此不适合验证多个控制器的网络，且其仅支持IP转发规则。这个缺陷使得Veriflow难以扩展到大型网络，而Libra改进了这一缺陷，它可以验证超大型网络[38]。Libra记录来自路由进程的网络事件流，并提供一种算法来捕获大规模网络中的表和一致的数据平面快照，将验证任务简化为更小的并行计算。NetPlumber提供了一种灵活的方式来表达和检查复杂的策略查询，而无需像HSA所要求的那样为每次策略检查编写新的临时代码。所以它能增量的检查状态变化是否符合规范并能够进行实时检查更新。NetPlumber将网络建模为节点，并在规则之间建立依赖图，即规则依赖图。网络不变量等价地转换为可达性断言。一旦网络发生变化，它将更新相应的网络依赖关系图，并重新进行所有形式的验证。一旦发现违规行为，NetPlumber将阻止更改。它不仅可以定义简单的不变量（包丢失和循环），而且还支持灵活的策略定义。但是NetPlumber无法适用于链路频繁更改的网络。Veriflow与NetPlumber仍然面临搜索空间过大的问题。AP Verifier将等价类采用BDD表示，称为原子谓词，开发了一种计算原子谓词集的算法，并增加了对ACL规则的支持[39]。原子谓词的使用大大加快了网络可达性的计算，使得AP Verifier比NetPlumber、VeriFlow更有效。但是，AP Verifier对等价类的更新性能较差，每个等价类更新消耗的时间可达10毫秒。另一方面，VeriFlow与NetPlumber都是定制化的代码，难以扩展到新的数据包格式和协议。而网络验证需要发展成为一个更标准、更扩展的技术。为解决该挑战，研究人员提出了NOD。NOD使用Datalog对策略和协议行为编码，能够进行通用的扩展，最后使用基于SMT Solver 技术的Z3 Datalog 框架进行验证。实验表明，NOD的Datalog 模型计算可达数据集合比模型检测和SMT 计算单个可达数据都快，相比于基于HSA的Hassel工具，虽然速度较慢，但更易于通用化。为了在实际系统中发挥作用，就需要在毫秒级的时间内检测到策略违规行为。由于NOD采用的是静态验证且速度较慢，因此无法满足实时网络验证的需求。

为了在实际应用中进行实时验证，大多数验证工具(如HAS，Veriflow)至少利用以下两个观察结果中的一个：a. 只有一小部分网络会受到数据平面的典型更改的影响；b.在整个网络中很多不同的数据包通常会有相同的转发动作。第一条产生了增量的网络验证方法；第二条则意味着可以用包等价类的形式对网络包的代表性子集进行分析，但是第二条也同样带来了等价类爆炸的问题，等价类爆炸严重限制了Veriflow的性能。Delta-net利用了第三个特性：通过数据包在部分网络中（不是全部网络）的网络转发行为之间的相似性，来实现高效的验证[41]。Delta-net提出了一种可证明的摊销准线性算法，解决了Veriflow中的等价类爆炸问题。实验证明在验证规则更新上，Delta-net比Veriflow速度快10倍以上。虽然Delta-net亚毫秒级的验证时间，但是它与AP Verifier和Veriflow一样只用于纯转发设备。它们的网络模型不能完全表达由转发以外的各种功能组成的真实设备，并且它们使用的算法也不能扩展到真实设备上。为了解决上述的问题，APKeep以逻辑功能的粒度来建模网络，而不是物理设备。每个功能，例如转发、过滤、重写，都被建模为一个逻辑独立的元素，它持有一组逻辑端口，对应于数据包上的不同动作[42]。因此APKeep能够在真实设备中支持通用功能和特定于供应商的功能组合。此外，APKeep 仅在必要时创建ECs，并尽可能地合并ECs,使得在更新过程中始终保持最小的ECs数量。实验表明，APKeep相比于VeriFlow、AP Verifier和Delta-net等，能在微秒级的时间内完成一条IP规则的验证，且能有效的在多规则验证下保证实时性要求。

（c）配置验证工作展望

现有的网络配置验证工作仍然面临着许多挑战。现将这些挑战以及未来的配置验证工作展望总结如下。

（1）错误配置定位

数据平面验证工具很难根据验证错误回溯到控制平面的准确位置，而现有的控制平面验证工具在发现配置错误以后并没有定位到准确的错误配置位置。除此之外，RealConfig虽然对控制平面进行了增量计算，但是它随后通过控制平面模拟出数据平面，在数据平面进行验证。根据验证结果，RealConfig不能提供准确的配置错误位置。与此同时，其它的配置验证工具并不支持增量配置验证。因此，拟开展控制平面增量验证以及错误配置定位研究。提出了一个控制平面增量验证工具ICPTree，它能够增量计算配置更新并能够定位错误配置位置。ICPTree的整体设计如图1所示。ICPTree采用Differential Datalog动态地维护整个控制平面，并生成一棵偏好树。ICPTree把配置变动作为输入，增量地计算配置变更并同时对偏好树进行修改。当修改结束后，结合意图进行验证。

（2）配置错误根因分析

最新的研究重点在配置增量验证(RealConfig)、扩大网络验证范围(Tiramisu)等，并且现有工具仅仅输出策略(意图)是否违反，或者验证出错时的反例。操作人员根据信息修改配置，没有工具可以给出配置的错误分析，即错误产生的根本原因。因此，拟开展配置错误根因分析研究。提出了一个贯穿控制平面和数据平面的验证工具进行配置错误根因分析。其整体流程如图2所示.

将数据平面(DP)快照，配置，策略，拓扑作为工具输入。随后将DP快照与配置通过图模型分别进行数据平面和控制平面建模，数据平面模型捕获等价类在网络中的实际行为，控制平面模型捕获配置构件之间的交互。通过数据平面模型、控制平面模型不断进行交互分析得到二者模型之间的差异，并最终确定配置错误原因。此外，为解决当前修复工具可伸缩的问题，可通过错误原因限制配置修复范围，以此加速修复。

（3）配置的可解释性增量验证

同一网络中往往涉及很多不同厂商的设备，如采用其他厂商的设备作为备用路由。现有的配置综合工具并没有对生成的配置进行解释，验证工具也没有对验证结果以及配置出错范围进行解释，操作人员很难仅通过观察配置从而确定出错情况并给予修改。基于此，提出对控制平面和验证输出应具有可解释性。

由于设备、配置之间的关系关联非常严格，整个配置可以看作是关系的集合体。知识图谱作为表示事物之间关系的成熟工具，已经在表示、解决事物关系方面得到了广泛的使用。此外，知识图谱还具有高表达性、高可扩展性、支持动态修改、利于使用图算法进行验证、允许逻辑推理等特性。因此，提出采用知识图谱对网络控制平面建模，并通过对错误的定位和易于理解的输出，提供对网络验证的可解释性。提出的基于知识图谱的可解释控制平面增量验证工具整体设计如图3所示。

（4）BGP配置意图推理

现有的验证工具大多在验证网络的不变量，如可达性，循环，黑洞等，而符合不变量的网络不一定符合网络管理员的设计意图，如流量没有从管理员规定的设备导出。现有的推理管理员意图的工具有Config2spec[23]、SEFSTARTER、Anime[24]。Config2spec在控制平面和数据平面上挖掘网络上流量的可达性，隔离性，航路点和路径平衡，这些特点不能表现出网络管理员的策略意图。SEFSTARTER依赖配置的相似性发现异常的、可能不符合管理员意图的配置，但是不能推理出管理员的意图。Anime根据网络上的路径推导管理员的意图，但是它使用的路径本身就有可能违反管理员的意图，不能保证推理出来的意图的正确性。因此，缺乏一种能正确推理出管理员的意图并发现网络中违反意图的配置的工具。BGP是基于策略的协议，管理员使用BGP协议宏观调控其流量走向，实现其意图，而与路径的长度无关。

因此，拟通过一种自动的方法，从BGP网络配置推断高级意图，并识别异常的网络配置，整体设计如图4。首先，使用SPVP生成BGP的稳定路径，生成带有下一跳信息的拓扑图；接着在此拓扑图推测用户意图，根据这些意图的特征，找出与管理员意图冲突的前缀；最后，修复这些前缀有关的意图，并生成有问题的配置提示。

参考文献

[1]    Walker D. Frenetic: A Network Programming Language[J]. Acm SigplanNotices, 2011, 46(9):279-291. 

[2]    Anderson C J, Foster N, Guha A, et al. NetKAT: Semantic foundations fornetworks[J]. Acm sigplan notices, 2014, 49(1): 113-126.

[3]    Subramanian K, Akella A. Genesis: Synthesizing Forwarding Tables inMulti-tenant Networks. In Proceedings of the 44th ACM SIGPLAN Symposium onPrinciples of Programming Languages POPL. 2017(17).

[4]    Beckett R, Mahajan R, Millstein T, et al. Don’t Mind the Gap: BridgingNetwork-wide Objectives and Device-level Configurations. Conference on AcmSigcomm Conference. ACM, 2016.

[5]    Beckett R, Mahajan R, Millstein T, et al. Network configuration synthesiswith abstract topologies[C]. Proceedings of the 38th ACM SIGPLAN Conference onProgramming Language Design and Implementation, 2017: 437-451.

[6]    Elhassany A, Tsankov P, Vanbever L, & Vechev M. Network-wideconfiguration synthesis. 2016: 261-281.

[7]    El-Hassany A, Tsankov P, Vanbever L, et al. Netcomplete: Practicalnetwork-wide configuration synthesis with autocompletion[C]. 15th {USENIX}Symposium on Networked Systems Design and Implementation ({NSDI} 18), 2018:579-594.

[8]    Kuo-Feng Hsu , Ryan Beckett , Ang Chen, Jennifer Rexford , PraveenTammana, David Walker, Contra: A Programmable System for Performance-awareRouting. NSDI 2020. Santa Clara, CA, USA (February 2020)

[9]    Saha S, Prabhu S, Madhusudan P. NetGen: Synthesizing data-planeconfigurations for network policies. Proceedings of the 1st ACM SIGCOMMSymposium on Software Defined Networking Research. ACM, 2015: 17.

[10]  Tian B, Zhang X, Zhai E, et al. Safely and automatically updatingin-network ACL configurations with intent language. Proceedings of the ACMSpecial Interest Group on Data Communication. ACM, 2019: 214-226.

[11]  Sabandal M M I, Schäfer E, Aed J, et al. Simvastatin induces adverseeffects on proliferation and mineralization of human primary osteoblasts[J].Head & face medicine, 2020, 16(1): 1-9.

[12]  Schneider T, Birkner R, Vanbever L. Snowcap: synthesizing network-wideconfiguration updates[C]//Proceedings of the 2021 ACM SIGCOMM 2021 Conference.2021: 33-49.

[13]  Kiran M, Pouyoul E, Mercian A, et al. Enabling intent to configurescientific networks for high performance demands[J]. Future Generation ComputerSystems, 2018, 79: 205-214.

[14]  Liao B, Gao J. An automatic policy refinement mechanism for policy-drivengrid service systems. In: Proc. of the Int’l Conf. on Grid and CooperativeComputing. Berlin, Heidelberg: Springer-Verlag, 2005. 166−171.

[15]  Riftadi M, Kuipers F. P4I/O: Intent-based networking with P4. In: Proc. ofthe 2019 IEEE Conf. on Network Softwarization (NetSoft). IEEE, 2019. 438−443.

[16]  Beigi MS, Calo S, Verma D. Policy transformation techniques inpolicy-based systems management. In: Proc. of the 5th IEEE Int’l Workshop onPolicies for Distributed Systems and Networks (POLICY 2004). IEEE, 2004. 13−22.

[17]  Jacobs A S , Pfitscher, Ricardo José, Ferreira R A , et al. RefiningNetwork Intents for Self-Driving Networks[J]. 2018:15-21.

[18]  Xu X , Liu C , Song D . SQLNet: Generating Structured Queries From NaturalLanguage Without Reinforcement Learning[J]. 2017.

[19]  Hwang W , Yim J , Park S , et al. A Comprehensive Exploration on WikiSQLwith Table-Aware Word Contextualization[J]. 2019.

[20]  D·乔拉发基斯, V·李, B·苏尔塔尼扎德赫,等. 网络设备间配置文件的翻译: CN, CN1615480 A[P].

[21]  Fogel A, Fung S, Pedrosa L, et al. A general approach to networkconfiguration analysis[C]//12th {USENIX} symposium on networked systems designand implementation ({NSDI} 15). 2015: 469-483.

[22]  Gember-Jacobson A, Viswanathan R, Akella A, et al. Fast control planeanalysis using an abstract representation[C]//Proceedings of the 2016 ACMSIGCOMM Conference. 2016: 300-313.

[23]  Fayaz S K, Sharma T, Fogel A, et al. Efficient network reachabilityanalysis using a succinct control plane representation[C]//12th {USENIX}Symposium on Operating Systems Design and Implementation ({OSDI} 16). 2016:217-232.

[24]  Weitz K, Woos D, Torlak E, et al. Scalable verification of border gatewayprotocol configurations with an SMT solver[C]//Proceedings of the 2016 ACMSIGPLAN International Conference on Object-Oriented Programming, Systems,Languages, and Applications. 2016: 765-780.

[25]  Beckett R, Gupta A, Mahajan R, et al. A general approach to networkconfiguration verification[C]//Proceedings of the Conference of the ACM SpecialInterest Group on Data Communication. 2017: 155-168.

[26]  Prabhu S, Chou K Y, Kheradmand A, et al. Plankton: Scalable networkconfiguration verification through model checking[C]//17th {USENIX} Symposiumon Networked Systems Design and Implementation ({NSDI} 20). 2020: 953-967.

[27]  Abhashkumar A, Gember-Jacobson A, Akella A. Tiramisu: Fast multilayernetwork verification[C]//17th {USENIX} Symposium on Networked Systems Designand Implementation ({NSDI} 20). 2020: 201-219.

[28]  Steffen S, Gehr T, Tsankov P, et al. Probabilistic verification of networkconfigurations[C]//Proceedings of the Annual conference of the ACM SpecialInterest Group on Data Communication on the applications, technologies,architectures, and protocols for computer communication. 2020: 750-764.

[29]  Kakarla S K R, Tang A, Beckett R, et al. Finding network misconfigurationsby automatic template inference[C]//17th {USENIX} Symposium on NetworkedSystems Design and Implementation ({NSDI} 20). 2020: 999-1013.

[30]  Ye F, Yu D, Zhai E, et al. Accuracy, Scalability,Coverage: A Practical Configuration Verifier on a Global WAN[C]//Proceedings ofthe Annual conference of the ACM Special Interest Group on Data Communicationon the applications, technologies, architectures, and protocols for computercommunication. 2020: 599-614.

[31]  Beckett R, Gupta A, Mahajan R, et al. Abstractinterpretation of distributed network control planes[J]. Proceedings of the ACMon Programming Languages, 2019, 4(POPL): 1-27.

[32]  Zhang P, Huang Y, Gember-Jacobson A, et al. Incremental NetworkConfiguration Verification[C]//Proceedings of the 19th ACM Workshop on HotTopics in Networks. 2020: 81-87.

[33]  Mai, Haohui, et al. "Debugging the data plane with anteater."ACM SIGCOMM Computer Communication Review 41.4 (2011): 290-301.

[34]  Kazemian, Peyman, George Varghese, and Nick McKeown. "Headerspace analysis: Static checking for networks." 9th {USENIX} Symposium onNetworked Systems Design and Implementation ({NSDI} 12). 2012.

[35]  Son, Sooel, et al. "Model checking invariant securityproperties in OpenFlow." 2013 IEEE international conference oncommunications (ICC). IEEE, 2013.

[36]  Khurshid, Ahmed, et al. "Veriflow: Verifying network-wide invariantsin real time." 10th {USENIX} Symposium on Networked Systems Design andImplementation ({NSDI} 13). 2013.

[37]  Kazemian, Peyman, etal. "Real time network policy checking using header space analysis."10th {USENIX} Symposium on Networked Systems Design and Implementation ({NSDI}13). 2013.

[38]  Zeng, Hongyi, et al. "Libra: Divide and conquer to verify forwardingtables in huge networks." 11th {USENIX} Symposium on Networked SystemsDesign and Implementation ({NSDI} 14). 2014.

[39]  Yang, Hongkun, andSimon S. Lam. "Real-time verification of network properties using atomicpredicates." IEEE/ACM Transactions on Networking 24.2 (2015): 887-900.

[40]   Lopes, Nuno P., et al. "Checking beliefs in dynamicnetworks." 12th {USENIX} Symposium on Networked Systems Design andImplementation ({NSDI} 15). 2015

[41]      Horn, Alex, AliKheradmand, and Mukul Prasad. "Delta-net: Real-time network verificationusing atoms." 14th {USENIX} Symposium on Networked Systems Design andImplementation ({NSDI} 17). 2017.

[42]       Zhang,Peng, et al. "APKeep: Realtime verification for real networks." 17th{USENIX} Symposium on Networked Systems Design and Implementation ({NSDI} 20).2020.

[43]  Birkner R,Drachsler-Cohen D, Vanbever L, et al. Config2Spec: Mining networkspecifications from network configurations[C]//17th {USENIX} Symposium onNetworked Systems Design and Implementation ({NSDI} 20). 2020: 969-984.

[44]  Kheradmand A.Automatic inference of high-level network intents by mining forwardingpatterns[C]//Proceedings of the Symposium on SDN Research. 2020: 27-33.