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

NSDI

1.  VeriFlow: Verifying Network-Wide Invariants in Real Time (2013)

Abstract—Networks are complex and prone to bugs.Existing tools that check network configuration files and the data-plane stateoperate offline at timescales of seconds to hours, and cannot detect or preventbugs as they arise. Is it possible to check network-wide invariants in realtime, as the network state evolves? The key challenge here is to achieveextremely low latency during the checks so that network performance is notaffected. In this paper, we present a design, VeriFlow, which achieves thisgoal. VeriFlow is a layer between a software- defined networking controller andnetwork devices that checks for network-wide invariant violations dynamicallyas each forwarding rule is inserted, modified or deleted. VeriFlow supportsanalysis over multiple header fields, and an API for checking custominvariants. Based on a prototype implementation integrated with the NOXOpenFlow controller, and driven by a Mininet OpenFlow network and Route Viewstrace data, we find that VeriFlow can perform rigorous checking within hundredsof microseconds per rule insertion or deletion.

摘要：网络很复杂且容易出错。检查网络配置文件和数据平面状态的现有工具能在几秒到几小时的时间范围内离线运行，并且不能检测或防止出现错误。随着网络状态的演变，是否有可能实时检查网络范围内的不变量？这里的关键挑战是在检查期间实现极低的延迟，以便网络性能不受影响。在本文中，我们提出了一个实现这一目标的设计。VeriFlow是软件定义的网络控制器和网络设备之间的一层，它在插入、修改或删除每个转发规则时动态检查网络范围内的不变违规。VeriFlow支持对多个标题字段的分析，以及用于检查自定义不变量的应用编程接口。基于与NOX OpenFlow控制器集成的原型实现，并由Mininet OpenFlow网络和路由视图跟踪数据驱动，我们发现VeriFlow可以在每次规则插入或删除的数百微秒内执行严格的检查。

动机：

(i) 现有的检测网络的技术如静态分析数据平面快照的方式虽然能检查出错误，但是方法是脱机离线的因此只能在错误发生之后发现。

(ii) 论文基于此问题引出“随着网络的发展，是否有可能实时检查整个网络的正确性?”并以实现增量实时验证网络正确性为目标。

贡献：

(i) 提出了一种实时网络数据平面验证方法VeriFlow，实现了对网络不变量进行实时验证的目标。

(ii) 基于SDN网络，实现并布置于SDN控制器于网络数据平面之间的，并提出了实现对网络不变量（可达性，回路，黑洞等）验证的算法，通过捕获控制器传来的信息，对规则插入设备或从设备中删除之前进行检查来验证不变量。

概述：

(i) 对于每一条规则的插入或移除消息，VeriFlow必须高效快速的验证这条规则产生的影响。前人的方法都需要数秒至数小时的时间。与前人不同的是在每次变化发生不会去检查整个网络。而是分成三步来验证：(a)根据新的规则和任何已存在的重叠的规则，将网络划分成一组基于IP范围的等价类（EC）的数据包，每个EC表示具有相同转发行为的包，网络中的每次变化通常只会影响一小部分的EC。因此，可以发现一组会被规则改变的EC，而验证网络不变量只需要在这些EC上进行;(b)Veriflow对每个被修改的EC建立单独的转发图，来代表网络转发行为;(c)通过遍历这些图（或运行自定义的用户定义代码）来确定不变量状态。

(ii) VeriFlow虽然做到了对数据平面进行实时验证，但是其不足在于，仅关注了IP转发规则，对其他规则不适用，缺乏对网络的建模，同时不能处理动态变化的网络配置。

NSDI

1. VeriFlow: Verifying Network-Wide Invariants in Real Time (2013)   Abstract—Networks are complex and prone to bugs. Existing tools that check network configuration files and the data-plane state operate offline at timescales of seconds to hours, and cannot detect or prevent bugs as they arise. Is it possible to check network-wide invariants in real time, as the network state evolves? The key challenge here is to achieve extremely low latency during the checks so that network performance is not affected. In this paper, we present a design, VeriFlow, which achieves this goal. VeriFlow is a layer between a software- defined networking controller and network devices that checks for network-wide invariant violations dynamically as each forwarding rule is inserted, modified or deleted. VeriFlow supports analysis over multiple header fields, and an API for checking custom invariants. Based on a prototype implementation integrated with the NOX OpenFlow controller, and driven by a Mininet OpenFlow network and Route Views trace data, we find that VeriFlow can perform rigorous checking within hundreds of microseconds per rule insertion or deletion.  

摘要：网络很复杂且容易出错。检查网络配置文件和数据平面状态的现有工具能在几秒到几小时的时间范围内离线运行，并且不能检测或防止出现错误。随着网络状态的演变，是否有可能实时检查网络范围内的不变量？这里的关键挑战是在检查期间实现极低的延迟，以便网络性能不受影响。在本文中，我们提出了一个实现这一目标的设计。VeriFlow是软件定义的网络控制器和网络设备之间的一层，它在插入、修改或删除每个转发规则时动态检查网络范围内的不变违规。VeriFlow支持对多个标题字段的分析，以及用于检查自定义不变量的应用编程接口。基于与NOX OpenFlow控制器集成的原型实现，并由Mininet OpenFlow网络和路由视图跟踪数据驱动，我们发现VeriFlow可以在每次规则插入或删除的数百微秒内执行严格的检查。  

动机： (i) 现有的检测网络的技术如静态分析数据平面快照的方式虽然能检查出错误，但是方法是脱机离线的因此只能在错误发生之后发现。 (ii) 论文基于此问题引出“随着网络的发展，是否有可能实时检查整个网络的正确性?”并以实现增量实时验证网络正确性为目标。  

贡献： (i) 提出了一种实时网络数据平面验证方法VeriFlow，实现了对网络不变量进行实时验证的目标。 (ii) 基于SDN网络，实现并布置于SDN控制器于网络数据平面之间的，并提出了实现对网络不变量（可达性，回路，黑洞等）验证的算法，通过捕获控制器传来的信息，对规则插入设备或从设备中删除之前进行检查来验证不变量。

   概述： (i) 对于每一条规则的插入或移除消息，VeriFlow必须高效快速的验证这条规则产生的影响。前人的方法都需要数秒至数小时的时间。与前人不同的是在每次变化发生不会去检查整个网络。而是分成三步来验证：(a)根据新的规则和任何已存在的重叠的规则，将网络划分成一组基于IP范围的等价类（EC）的数据包，每个EC表示具有相同转发行为的包，网络中的每次变化通常只会影响一小部分的EC。因此，可以发现一组会被规则改变的EC，而验证网络不变量只需要在这些EC上进行;(b)Veriflow对每个被修改的EC建立单独的转发图，来代表网络转发行为;(c)通过遍历这些图（或运行自定义的用户定义代码）来确定不变量状态。 (ii) VeriFlow虽然做到了对数据平面进行实时验证，但是其不足在于，仅关注了IP转发规则，对其他规则不适用，缺乏对网络的建模，同时不能处理动态变化的网络配置。  

2. A General Approach to Network Configuration Analysis (2015)  

Abstract—We present an approach to detect network configuration errors, which combines the benefits of two prior approaches. Like prior techniques that analyze configuration files, our approach can find errors proactively, before the configuration is applied, and answer “what if” questions. Like prior techniques that analyze data-plane snapshots, our approach can check a broad range of forwarding properties and produce actual packets that violate checked properties. We accomplish this combination by faithfully deriving and then analyzing the data plane that would emerge from the configuration. Our derivation of the data plane is fully declarative, employing a set of logical relations that represent the control plane, the data plane, and their relationship. Operators can query these relations to understand identified errors and their provenance. We use our approach to analyze two large university networks with qualitatively different routing designs and find many misconfigurations in each. Operators have confirmed the majority of these as errors and have fixed their configurations accordingly.  

摘要：提出了一种检测网络配置错误的方法Batfish，结合和现存两种方法的优点。和现有技术验证配置文件方法类似，可以主动去在配置得到应用前发现错误，也可以像现有技术验证数据平面快照一样，检查一个广阔范围的转发属性并生成违反检查属性的实际数据包。通过推导是两种方法相结合，使用一组逻辑关系代表控制平面，数据平面及其关系。该方法已在两个大型网络应用并发现了许多配置错误。   动机： (i) 配置验证领域已经出现了众多控制平面或数据平面的验证技术，但这两方面的技术都各自有自己的优缺点，现有技术无法同时主动的检查出违反故障一致性和多路径一致性的错误。 (ii) 以前的研究不能搞定多个不同协议共存以及新协议插入的问题，因为它们提出的只是针对固定场景，如只使用ACL。  

贡献： (i) 开发了一种新方法和实用工具Batfish来分析网络配置。它同时包含控制平面和数据平面两方面验证，结合两方优点从而解决双方各自不能解决的问题。 (ii) 经过试验评估表面Batfish能够检查出现有技术各自不能检查出的错误。 (iii) 工具是开源公开的，以供他人使用和探索新用例。  

概述：Batfish工作流程有四个阶段如图2所示。 (i) 12阶段通过给定的配置转换成具体的数据平面，阶段1通过给定的配置和拓扑传给控制平面生成器生成控制平面模型，其中控制平面模型被一组数据记录变体LogiQL定义，是LogicBloc引擎的语言，除了基本的数据记录，LogiQL还支持整数，算术运算，聚合等。 (ii) 后两个阶段识别并本地化配置错误，在阶段3中通过分析多个数据平面模型来检查所需正确属性，该工具可以通过一阶逻辑表达式来表示一个或多个数据平面的关系，通过将数据平面关系和正确性属性转换成Z3约束求解器来实现。阶段4通过溯源探测结合数据平面模型来找出错误出现的配置的特定行。 

不足： Batfish将网络配置和多个给定环境作为输入，模拟控制平面，最终生成相应的数据平面。然后，利用现有的数据平面工作来检查错误配置。基于模拟的工作在考虑大型网络中的不确定性(例如，k-failure tolerance)时会遇到可伸缩性问题。  

3. Delta-net: Real-time Network Verification Using Atoms (2017)   Abstract—Real-time network verification promises to automatically detect violations of network-wide reachability invariants on the data plane. To be useful in practice, these violations need to be detected in the order of milliseconds, without raising false alarms. To date, most real-time data plane checkers address this problem by exploiting at least one of the following two observations: (i) only small parts of the network tend to be affected by typical changes to the data plane, and (ii) many different packets tend to share the same forwarding be haviour in the entire network. This paper shows how to effectively exploit a third characteristic of the problem, namely: similarity among forwarding be haviour of packets through parts of the network, rather than its entirety. We propose the first provably amortized quasi-linear algorithm to do so. We implement our algorithm in a new real-time data plane checker, Delta-net. Our experiments with SDN-IP, a globally deployed ONOS software-defined networking application, and several hundred million IP prefix rules generated using topologies and BGP updates from real world deployed networks, show that Delta-net checks a rule insertion or removal in approximately 40 microseconds on average, a more than 10× improvement over the state-of-the-art. We also show that Delta-net eliminates an inherent bottleneck in the state-of-the-art that restricts its use in answering Datalog-style “what if” queries.  

摘要：实时网络验证有望自动检测数据平面上违反网络范围可达性不变量的情况。为了在实践中有用，需要以毫秒为单位检测这些违规，而不会产生错误警报。迄今为止，大多数实时数据平面检查器通过利用以下两种观察中的至少一种来解决这个问题:(1)只有网络的一小部分倾向于受到数据平面的典型变化的影响，以及(2)许多不同的分组倾向于在整个网络中共享相同的转发行为。本文展示了如何有效地利用问题的第三个特征，即:通过网络的一部分而不是整个网络的数据包转发行为之间的相似性。为此，我们提出了第一个可证明摊销的拟线性算法。我们在一个新的实时数据平面检查器中实现了我们的算法。我们对SDN-IP(一种全球部署的ONOS软件定义的网络应用程序)和使用拓扑结构生成的数亿个IP前缀规则以及来自真实世界部署网络的BGP更新进行的实验表明，Delta-net平均在大约40微秒内检查规则的插入或删除，比现有技术提高了10倍以上。我们还表明，Delta-net消除了现有技术中限制其在回答数据日志式“What-if”查询时使用的固有瓶颈。  

动机： (i) 现有技术并不能高效的处理涉及大量包等价类的操作，从而限制了对网络故障的实时性分析，并且从本质上限制了数据平面检查器用最近的提出的数据日志方法来实现对链路故障(What-if)分析。 (ii) 现有的实时数据平面验证技术（如Veriflow）仍然有其固有的瓶颈，如不能回答更广泛问题，对不变量的验证不够高效能够。

  贡献： (i) 提出Delta-net，一种增量验证的实时数据平面验证方法，通过维护网络中数据包流的紧凑表示，从而支持更广泛的场景和查询。提供了基于全球部署的SDN应用，新的现实基准的开源代码。 (ii) 与现有技术（Veriflow）生成大量转发图的方式来验证不变量不同的是，Delta-net通过增量更新并维护一个边标签图来实现验证不变量，大大减少了验证时间。 (iii) 实验证明在验证规则更新上Delta-net比现有技术速度快10倍以上，并能回答消耗昂贵的链路故障（what if）类问题。  

  4. Tiramisu: Fast Multilayer Network Verification (2020)   Abstract—Today’s distributed network control planes are highly sophisticated, with multiple interacting protocols operating at layers 2 and 3. The complexity makes network configurations highly complex and bug-prone. State-of-the-art tools that check if control plane bugs can lead to violations of key properties are either too slow, or do not model common network features. We develop a new, general multilayer graph control plane model that enables using fast, property-customized verification algorithms. Our tool, Tiramisu can verify if policies hold under failures for various real-world and synthetic configurations in < 0.08s in small networks and < 2.2s in large networks. Tiramisu is 2-600X faster than state-of-the-art without losing generality.  

摘要：现在的分布式网络在第2层和第3层有多个交互协议，控制平面非常复杂。网络的复杂性使得网络配置变得非常复杂并且容易出现错误。检查控制平面错误是否会导致关键属性违反的最先进的工具要么太慢，要么不能模拟常见的网络特性。我们开发了一种新的、通用的多层图控制平面模型，该模型能够使用快速的、自定义属性的验证算法。我们的工具Tiramisu可以验证各种真实世界和合成配置在故障下策略的支持情况，在小型网络中时间低于0.08秒，在大型网络中时间在2.2秒内。Tiramisu在不失去普遍性的前提下比最先进的技术快2-600倍。  

动机： (i) 网络的复杂性使得网络配置变得非常复杂并且容易出错。 (ii) 现在的验证工具往往在性能和通用性两方面进行舍去，基于图的控制平面验证速度快但不通用，基于符号和显式状态模型验证器通用但速度不快。

  贡献： (i) Tiramisu将编码和验证算法解耦。 (ii) Tiramisu利用一种新的、丰富的网络编码，为各种控制平面特性和网络设计构建模型。 (iii) Tiramisu可以为不同类别的策略使用不同的自定义验证算法，大大提高了性能。

  5. Plankton: Scalable network configuration verification through model checking (2020)   Abstract—Network configuration verification enables operators to ensure that the network will behave as intended, prior to deployment of their configurations. Although techniques ranging from graph algorithms to SMT solvers have been proposed, scalable configuration verification with sufficient protocol support continues to be a challenge. In this paper, we show that by combining equivalence partitioning with explicit-state model checking, network configuration verification can be scaled significantly better than the state of the art, while still supporting a rich set of protocol features. We propose Plankton, which uses symbolic partitioning to manage large header spaces and efficient model checking to exhaustively explore protocol behavior. Thanks to a highly effective suite of optimizations including state hashing, partial order reduction, and policy-based pruning, Plankton successfully verifies policies in industrial-scale networks quickly and compactly, at times reaching a 10000× speedup compared to the state of the art.  

摘要：网络配置验证使操作人员能够在部署配置之前确保网络将按预期运行。尽管已经提出了从图算法到SMT求解器的各种技术，但具有足够协议支持的可伸缩配置验证仍然是一个挑战。在本文中我们证明，通过将等价类划分与显示状态模型检查相结合，网络配置验证可以比目前的技术水平更好地扩展，同时仍然支持丰富的协议属性。我们推荐使用符号区分来管理较大的头文件空间和高效的模型检查来探测协议行为。通过一套实用的优化（包括状态散列、部分订单减少和基于策略修剪），Plankton能快速验证工业规模网络中的策略，有时比目前技术水平提高1万倍。   动机： (i) 确保网络的正确性是一项困难而关键的任务。 (ii) 当前的验证工具不能支持广泛的协议并对协议进行扩展。  

贡献： (i) 定义了一种配置验证范式，即结合数据包等价计算和显示状态模型检查。 (ii) 进行优化使设计对实际规模网络可行，其中包括减少事件探索空间和提高探索效率。 (iii) 实现Plankton，它支持OSPF、BGP和静态路由。根据实验结果，它可以在实际规模下验证策略（对包含300多个设备的网络验证时间低于1秒）并且Plankton在性能均超出本实验中的当前技术，有些情况可以超出4个数量级。  

Plankton设计： 图5 Plankton设计        第一阶段计算数据包等价类；然后依赖关系制定，即包等价类一旦计算，Plankton就计算它们间的依赖，依赖关系用有向图存储；然后使用显示状态模型检查器SPIN来检查；同时，可以进行策略验证。  

不足：Plankton进行了许多优化，到仍然需要枚举许多故障场景的状态空间并按顺序进行检查，所以时间可能会较长。Plankton基于数据包等价类方法在63个设备的真实网络单链路故障下验证可达性仅需要几秒钟，但对于有245个设备运行OSPF的合成的胖树拓扑验证需要3分钟。   

6. Config2Spec: Mining Network Specifications from Network Configurations (2020)  

Abstract—Network verification and configuration synthesis are promising approaches to make networks more reliable and secure by enforcing a set of policies. However, these approaches require a formal and precise description of the intended network behavior, imposing a major barrier to their adoption: network operators are not only reluctant to write formal specifications, but often do not even know what these specifications are.   We present Config2Spec, a system that automatically synthesizes a formal specification (a set of policies) of a network given its configuration and a failure model (e.g., up to two link failures). A key technical challenge is to design a synthesis algorithm which can efficiently explore the large space of possible policies. To address this challenge, Config2Spec relies on a careful combination of two well-known methods: data plane analysis and control plane verification.   Experimental results show that Config2Spec scales to mining specifications of large networks (>150 routers).  

摘要：网络验证和配置综合是使网络在一组策略下保证更加可靠和安全的方法。但是，这些方法需要对预期的网络行为进行正式和精确的描述，这给使用它们的用户造成一个障碍：网络运营商不仅不愿意编写正式的规范，甚至常常不知道这些规范是什么。我们提出Config2Spec，一个可以自动综合给定配置的网络的正式规范（一组策略）和故障模型（例如，最多两个链路故障）的系统。一个关键的技术挑战是设计一个综合算法，该算法能有效地探索可能的策略空间。为解决这一困难，Config2Spec采用两个知名方法的组合：数据平面分析和控制平面验证。实验结果表明，Config2Spec可扩展到大型网络（多于150台路由器）来挖掘规范。  

动机： (i) 获得网络行为的规范也是有用的。如，帮运营商识别不期望的行为和不一致性；根据新需求来平滑的过渡（更新）配置。 (ii) 目前一些工作已经通过观察数据平面内容来研究网络规范，但都局限于可达性策略，要么是近似的规范要么忽略故障对规范的影响。  

贡献： (i) 提出一种自动挖掘网络规范的方法，方法利用转发平面分析和控制平面验证； (ii) 设计动态的预测器，预测器动态决定可提供更高进展的方法； (iii) 设计策略感知采样器，查找能修剪更多策略的转发平面； (iv) 将策略分组和基于拓扑修剪以减少传给验证器的查询数量； (v) 完成端到端的实现并进行广泛评估，证明Config2Spec可以扩展到大型网络，性能显著优于基线。   Config2Spec工作过程： 图6 Config2Spec工作过程       

Config2Spec通过设计预测器来将数据面分析和控制平面验证结合起来，动态选择这两个方法，数据平面分析修剪了大量策略空间，控制平面验证避免对所有数据平面进行验证，从而快速挖掘网络规范。  

7. APKeep: Realtime Network Verification for Real Networks (2020)  

Abstract—Realtime network verification ensures the correctness of network by incrementally checking data plane updates in real time (e.g., < 1ms per rule update). Even state-of-the-art methods can already achieve sub-millisecond verification time, such speed is achieved mostly for pure IP forwarding devices, and is unrealistic for real-world networks, due to two reasons. (1) Their network models cannot express the forwarding behavior of real devices, which have various functions including IP forwarding, ACL, NAT, policy-based routing, etc. (2) Their update algorithms do not scale in space and/or time: multifield rules (e.g., ACL rules) can make these tools run out of memory and/or incur long verification time. To scale real-time verification to real networks, we propose APKeep based on a new modular network model that is expressive for real devices, and propose new algorithms that can achieve low memory cost and fast update speed at the same time. Our experiments show that for real-world update traces consisting of IP forwarding rules and ACL rules, existing methods either run out of memory or incur a prohibitively long verification time, while APKeep still achieves a sub-millisecond verification time. We also show that APKeep can verify an update of NAT rule mostly in less than 1 millisecond.  

摘要：实时网络验证通过实时增量检查数据平面更新（如，每次规则更新低于1毫秒）来确保网络的正确性。最先进的方法可以达到亚毫秒的验证时间，但是这样的速度是在纯IP转发设备中实现的，而对于真实网络来说是不切实际的，原因有两个：(1) 它们的网络模型无法表达真实设备的转发行为，真实设备具有IP转发、ACL、NAT、策略路由等多种功能。(2) 它们的更新算法在空间或时间上不具有伸缩性：多字段规则(如ACL规则)会使这些工具耗尽内存或导致较长的验证时间。为了将实时验证扩展到真实网络中，我们提出了一种新的模块化网络模型APKeep，该模型能够表达真实设备，并提出了新的算法，可以同时实现低内存成本和快速更新速度。我们的实验表明，对由IP转发规则和ACL规则组成的真实世界的更新跟踪，现有的方法要么是内存不足，要么是产生了令人难以忍受的长验证时间，而APKeep仍然可以实现亚毫秒的验证时间。我们还展示了APKeep可以在不到1毫秒的时间内验证NAT规则的更新。  

动机： (i) 现在实时验证的网络模型不能很好表达真实的设备。 (ii) 实时验证的算法那不能扩展到真实的设备。   贡献： (i) 提出了一种模块化的、可表达的网络模型，用于真实网络设备的建模。 (ii) 设计了APKeep，它使用新的算法快速更新网络模型，以实现实时验证。 (iii) 展示了APKeep对于由IP转发规则、ACL规则和NAT规则组成的更新跟踪实现了亚毫秒的验证时间。  

APKeep的系统结构： 图7 APKeep的系统结构        APKeep分为三层结构：驱动层、模型层和验证层。驱动层是网络转发平面和模型层的接口；模型层是APKeep的核心，模型构造器通过基于转发平面的配置创造元素来构建PPM模型，模型更新器通过顺序处理转发平面的每个更新来不断更新PPM模型。验证层在模型层上方执行验证程序。  

8. Finding Network Misconfigurations by Automatic Template Inference (2020)   Abstract—Network verification to detect router configuration errors typically requires an explicit correctness specification. Unfortunately, specifications often either do not exist, are incomplete, or are written informally in English. We describe an approach to infer likely network configuration errors without a specification through a form of automated outlier detection. Unlike prior techniques, our approach can identify outliers even for complex, structured configuration elements that have a variety of intentional differences across nodes, like access control lists, prefix lists, and route policies. Given a collection of configuration elements, our algorithm automatically infers a set of parameterized templates, modeling the (likely) intentional differences as variations within a template while modeling the (likely) erroneous differences as variations across templates. We have implemented our algorithm, which we call structured generalization, in a tool called SELFSTARTER and used it to automatically identify configuration outliers in a collection of datacenter networks from a large cloud provider, the wide-area network from the same cloud provider, and the campus network of a large university. SELFSTARTER found misconfigurations in all three networks, including 43 previously unknown bugs, and is in the process of adoption in the configuration management system of a major cloud provider.  

摘要：检测路由器配置错误的网络验证方法通常需要一个明确地正确规范，但规范常常不存在、不完整或用英文非正式地编写。本文描述一种不用规范来推断可能的网络配置错误的方法，该方法通过自动离群值检测来完成验证。和之前的技术不同，该方法可以识别复杂的结构化配置元素的离群值，这些元素在节点之间有差异，如访问控制列表、前缀列表和路由策略。 给定一组配置元素，本文的算法自动推断出一组参数化模板，并将可能的有意差异建模为模板中的变化，而将可能的错误差异建模为模板之间的变化。在SELFSTARTER中实现了我们称为结构化综合的算法，用它来自动识别来自大型云提供商的数据中心网络集合、同一云提供商的广域网以及大型学校的校园网的配置离群值。SELFSTARTER在三个网络中均发现了错误的配置，包括43个之前未知的错误，并且一个云提供商的配置管理系统正在使用。  

动机： (i) 路由器配置错误是造成网络中断的主要错误，许多验证方法需要明确的正确性规范来进行验证。 (ii) 一些工具不需要规范，但仅限于验证通用的配置错误（如转发循环、黑洞）等。   贡献： (i) 自动模板推断：据文章作者所说，他们是第一个提出网络配置段自动模板推断的思想，并利用该思想识别网络配置错误。 (ii) 结构化综合：提出了一种新的网络配置段参数化模板的自动推断算法，该算法结合了序列比对和两级结构中的互相匹配，以支持参数化和重排序的控制形式。 (iii) 实现：在名为SELFSTARTER的实用工具中实现了结构化综合。 (iv) 评价：SELFSTARTER在几个大型真实的生产网络中验证了它的高质量离群值和低误报率。  

9．Liveness Verification of Stateful Network Functions (2020)

Abstract—Network verification tools focus almost exclusively on various safety properties such as “reachability” invariants, e.g., is there a path from host A to host B? Thus, they are inapplicable to providing strong correctness guarantees for modern programmable networks that increasingly rely on stateful network functions. Correct operations of such networks depend on the validity of a larger set of properties, in particular liveness properties. For instance, a stateful firewall that only allows solicited external traffic works correctly if it eventually detects and blocks malicious connections, e.g., if it eventually blocks an external host E that tries to reach the internal host I before receiving a request from I. Alas, verifying liveness properties is computationally expensive and, in some cases, undecidable. Existing verification techniques do not scale to verify such properties. In this work, we provide a compositional programming abstraction, model the programs expressed in this abstraction using compact Boolean formulas, and show that verification of complex properties is fast on these formulas, e.g., for a 100-host network, these formulas result in 8 speedup in the verification of key properties of a UDP flood mitigation function compared to a naive baseline. We also provide a compiler that translates the programs written using our abstraction to P4 programs.  

摘要：网络验证工具几乎只关注各种安全属性，如可达性不变量（是否有从主机A到主机B的路径?）。因此，它们不能为越来越依赖有状态网络功能的现代可编程网络提供强大的正确性保证。这种网络的正确操作依赖于一组关键的活的属性的有效性。例如，检测并阻止恶意连接后，有状态防火墙才允许请求的外部通信正常工作，如：在防火墙收到主机I的请求前都会阻塞外部主机E到内部主机I的连接。验证活性属性在计算上是昂贵的，而且在某些情况下是无法确定的。现有的验证技术不能验证这些属性。在本文中，我们提供了一个组合的编程抽象，用布尔公式对这个抽象中表达的程序进行建模，并证明在这些公式上验证复杂属性是快速的。例如，针对一个100个主机的网络，使用这些公式对UDP泛洪缓解函数的关键属性的验证速度比之前快8倍。我们还提供了一个编译器，可以将使用我们的抽象编写的程序转换为P4程序。  

动机： (i) 当前的验证工具多验证可达性等通用的不变量，但这些方法不能验证有状态网络中的丰富的活的属性。  

贡献： (i) 为网络程序员提供了一个简洁的one-big-switch的抽象来表达他们的意图，这种抽象强制将不同网络功能的逻辑分离。 (ii) 将程序建模为一种紧密的“无包”数据结构，而不像常见的对数据包类的转发行为建模的方法，即，将包的概念抽象出来转而关注负责实现功能的实体：包处理规则。 (iii) 建立并评估本文系统的原型。评估表明，该编程模型能简洁地表达各种函数，验证的可扩展性比朴素的编码提高了数量级，说明大大提高了验证速度。  

10. NetSMC: A Custom Symbolic Model Checker for Stateful Network Verification (2020)  

Abstract—Modern networks enforce rich and dynamic policies (e.g., dynamic service chaining and path pinning) over a number of complex and stateful NFs (e.g., stateful firewall and load balancer). Verifying if those policies are correctly implemented is important to ensure the network’s availability, safety, and security. Unfortunately, theoretical results suggest that verifying even simple policies (e.g., A cannot talk to B) in stateful networks is undecidable. Consequently, any approach for stateful network verification has to fundamentally make some relaxations; e.g., either on policies supported, or the network behaviors it can capture, or in terms of the soundness/completeness guarantees. In this paper, we identify practical opportunities for relaxations in order to develop an efficient verification tool. First, we identify key domain-specific insights to develop a more compact network semantic model which is equivalent to a general semantic model for checking a wide range of policies under practical conditions. Second, we identify a restrictive-yet-expressive policy language to support a wide range of policies including dynamic service chaining and path pinning while enable efficient verification. Third, we develop customized symbolic model checking algorithms as our model and policy specification allows us to succinctly encode network states using existential first-order logic, which enables efficient checking algorithms. We prove the correctness of our approach for a subset of policies and show that our tool, NetSMC, achieves orders of magnitude speedup compared to existing approaches.  

摘要：现代网络在许多复杂的、有状态的网络功能(如有状态防火墙和负载均衡器)上强制执行丰富的动态策略(如动态服务链接和路径固定)。验证这些策略是否被正确实施对于确保网络的可用性、安全性和安全性非常重要。但是理论结果表明，在有状态的网络中，即使验证简单的策略(例如，A不能与B通信)也是无法确定的。因此，任何有状态网络验证的方法都必须从根本上进行一些放宽，如在支持的策略上、可以捕获的网络行为上或者在完整性保证方面。在这篇论文中，我们确定了放宽的机会以开发一个有效的验证工具。首先，我们利用特定领域的关键见解开发了一个紧凑的网络语义模型，该模型相当于一个通用语义模型，用于在实际条件下检查广泛的策略。其次，我们确定了一种限制但具有表达性的策略语言以支持广泛的策略（包括动态服务链接和路径固定），同时支持有效的验证。第三，我们开发了定制的符号模型检查算法，因为我们的模型和策略规范允许我们使用存在的一阶逻辑简洁地编码网络状态，这使检查算法成为可能。我们针对一组策略证明了我们方法的正确性，并表明我们的工具NetSMC与现有方法相比实现了数量级的加速。  

动机： (i) 现在的计算机网络部署了大量的复杂的有状态功能，如有状态防火墙、NAT到负载均衡器。但没有方法能够对这些有状态功能的属性进行有效验证。   贡献： (i) 利用特定领域的关键见解开发了一个紧凑的网络语义模型，该模型相当于一个通用语义模型，用于在实际条件下检查广泛的策略。 (ii) 确定了一种限制但具有表达性的策略语言以支持广泛的策略（包括动态服务链接和路径固定），同时支持有效的验证。开发了定制的符号模型检查算法，因为模型和策略规范允许使用存在的一阶逻辑简洁地编码网络状态，这使检查算法成为可能。  

SIGCOMM

1. Accuracy, Scalability, Coverage – A Practical Configuration Verifier on a Global WAN(2020)  

Abstract—This paper presents Hoyan– the first reported large scale deployment of configuration verification in a global-scale wide area network (WAN). Hoyan has been running in production for more than two years and is currently used for all critical configuration auditing and updates on the WAN. We highlight our innovative designs and real-life experience to make Hoyan accurate and scalable in practice. For accuracy under the inconsistencies of devices’ vendor-specific behaviors (VSBs), Hoyan continuously discovers the flaws in device behavior models, thus aiding the operators in fixing the models. For scalability to verify our global WAN, Hoyan introduces a “global-simulation & local formal-modeling” strategy to model uncertainties in small scales and perform aggressive pruning of possibilities during the protocol simulations. Hoyan achieves near-100% verification accuracy after it detected and fixed O(10) VSBs on our WAN. Hoyan has prevented many potential service failures resulting from misconfiguration and reduced the failure rate of updates of our WAN by more than half in 2019.  

摘要：本文介绍了Hoyan ——首次报道的在全球范围的广域网(W AN)中大规模部署配置验证技术。Hoyan已经在生产中运行了两年多，目前用于WAN上的所有关键配置审核和更新。我们强调创新的设计和真实的体验，使Hoyan在实践中具有准确性和可扩展性。为了在设备vendor-specific behavior (VSBs)不一致的情况下保持准确性，Hoyan不断发现设备行为模型的缺陷，从而帮助运营商对模型进行修正。为了验证我们的全局WAN的可扩展性，Hoyan引入了“全局模拟和局部形式化建模”策略，以在小尺度上建模不确定性，并在协议模拟期间执行积极的可能性修剪。Hoyan在我们的WAN上检测和修复了O(10) VSBs后，达到了接近100%的验证精度。2019年，Hoyan已经防止了许多由错误配置导致的潜在服务故障，并将我们WAN更新的故障率降低了一半以上。  

动机： (i) 为了维护一个阿里巴巴全球广域网，随着WAN变得越来越大、越来越复杂，以及应用程序对网络的需求越来越频繁地改变，维持这样一个大规模和复杂的WAN的可靠性是极具挑战性的，一个主要的风险来源是路由配置中的模糊错误，这违反了运营商的可达性意图,为了防止路由配置错误导致的事故,强烈地希望采用验证作为一种自动、快速和全面的方式来(a)审计当前配置快照中的隐藏错误;(b)在更新中检查新配置的正确性和不明显的歧义。  

贡献： (i) Hoyan是第一个考虑VSBs的配置验证器，并在生产环境中实现接近100%的准确性。 (ii) 由于其新颖的“全局仿真与局部形式化建模”设计，在验证不确定网络时具有良好的可扩展性。   概述：Hoyan有两个部分，如图8所示。 在前端，配置验证器结合当前在线配置和来自运营商的建议配置改变来生成要验证的目标配置。根据网络中每个设备的库存单位(或SKU)，获取每个设备的行为模型，并向它们提供目标配置以生成目标网络模型，之后，验证模块查询目标网络模型以回答操作员的验证问题。Hoyan为运营商提供了用户友好的界面来表达感兴趣的属性。基于运营需求和经验，Hoyan主要致力于验证可达性和角色平等的性质。广域网不需要验证隔离问题或黑洞等主要存在于数据通信网络中的属性。   在后端，行为模型调谐器(灰色框中的组件)持续收集在线配置和网络信息，包括路由表(RIB)和路由更新。阿里巴巴的内部系统将记录和维护上述信息。一方面，调谐器将这些配置传递给每个设备的行为模型，以生成在线网络模型(针对整个广域网)。另一方面，它调用验证器来检查它计算的模型和它收集的网络信息之间是否有任何不匹配。当发现不匹配时，调谐器定位到一个小的配置片段，以便人类可以容易地理解。网络运营商通常会编写一个小补丁来修复相应设备型号中的缺陷 图8

2. GRoot: Proactive Verification of DNS Configurations(2020)  

Abstract—The Domain Name System (DNS) plays a vital role in today’s Internet but relies on complex distributed management of records. DNS misconfiguration related outages have rendered popular services like GitHub, HBO, LinkedIn, and Azure inaccessible for extended periods. This paper introduces GRoot, the first verifier that performs static analysis of DNS configuration files, enabling proactive and exhaustive checking for common DNS bugs; by contrast, existing solutions are reactive and incomplete. GRoot uses a new, fast verification algorithm based on generating and enumerating DNS query equivalence classes. GRoot symbolically executes the set of queries in each equivalence class to efficiently find (or prove the absence of) any bugs such as rewrite loops. To prove the correctness of our approach, we develop a formal semantic model of DNS resolution. Applied to the configuration files from a campus network with over a hundred thousand records, GRoot revealed 109 bugs within seconds. When applied to internal zone files consisting of over 3.5 million records from a large infrastructure service provider, GRoot revealed around 160k issues of blackholing, initiating a cleanup. Finally, on a synthetic dataset with over 65 million real records, we find GRoot can scale to networks with tens of millions of records.  

摘要：域名系统(DNS)在当今的互联网中扮演着至关重要的角色，但它依赖于对记录的复杂分布式管理。与DNS错误配置相关的宕机导致GitHub、HBO、LinkedIn和Azure等流行服务长时间无法访问。本文介绍了第一个对DNS配置文件进行静态分析的验证器GRoot，它能够主动、彻底地检查常见的DNS错误;相比之下，现有的解决方案是反应性的和不完整的。GRoot使用了一种新的、快速的验证算法，基于生成和枚举DNS查询等价类。GRoot象征性地在每个等价类中执行一组查询，以有效地查找(或证明不存在)任何错误，如重写循环。为了证明我们方法的正确性，我们开发了一个正式的DNS解析语义模型。应用到校园网的配置文件中，有超过10万条记录，GRoot在几秒钟内就发现了109个漏洞。当应用到由大型基础设施服务提供商提供的超过350万条记录组成的内部区域文件时，GRoot揭露了大约16万个黑洞问题，启动了清理工作。最后，在一个有6500万条真实记录的合成数据集上，我们发现格鲁特可以扩展到拥有数千万条记录的网络。  

动机： (i) 编写和维护正确的DNS配置很有挑战性，原因在于(a)协议本质上的不确定导致查询DNS服务器返回不相同的结果;(b) DNS协议是复杂而微妙的，涉及多种类型的记录以及这些记录之间复杂的依赖关系，这是由于查询重写等行为造成的;(c) DNS被管理为分布式区域文件的集合，在不同组织的控制下;(d)所有这些问题都是在理解单个DNS查询的上下文中出现的，操作员必须确保所有可能的查询都按预期的方式运行。 (ii) 除了不确定性导致查询返回结果不同外，DNS行为可能在很多方面发送错误，比如配置错误可能导致DNS返回结果丢失，或者使查询陷入重写循环等。 (iii) 设计DNS的检查器目的在于及时发现配置错误并提供发现配出错误的有效性。  

贡献： (i) 提出了第一个正式的DNS模型，它既包含权威系统的语义，也包含递归系统的语义. (ii) 利用DNS形式化模型，描述并证明了一个快速生成等价类DNS查询的算法的正确性。这些等价类使GRoot能够有效地、详尽地检查DNS区域文件的正确性。 (iii) 对生产配合文件进行了有效评估，将GRoot评估使用在(a)配置的数据来自一个大型校园网络,(b)配置从一个大型基础设施服务提供者,和(c)合成数据集由超过6500万个网络记录,显示GRoot在发现bug和验证大型配置方面非常有效。  

3. Probabilistic Verification of Network Configurations(2020)   Abstract—Not all important network properties need to be enforced all the time. Often, what matters instead is the fraction of time / probability these properties hold. Computing the probability of a property in a network relying on complex inter-dependent routing protocols is challenging and requires determining all failure scenarios for which the property is violated. Doing so at scale and accurately goes beyond the capabilities of current network analyzers. In this paper, we introduce NetDice, the first scalable and accurate probabilistic network configuration analyzer supporting BGP, OSPF, ECMP, and static routes. Our key contribution is an inference algorithm to efficiently explore the space of failure scenarios. More specifically, given a network configuration and a property ϕ, our algorithm automatically identifies a set of links whose failure is provably guaranteed not to change whether ϕ holds. By pruning these failure scenarios, NetDice manages to accurately approximate P(ϕ). NetDice supports practical properties and expressive failure models including correlated link failures. We implement NetDice and evaluate it on realistic configurations. NetDice is practical: it can precisely verify probabilistic properties in few minutes, even in large networks.  

摘要：并不是所有重要的网络属性都需要一直执行。通常情况下，重要的是这些属性所占的时间/概率百分比。在一个依赖复杂的相互依赖路由协议的网络中，计算某个属性的概率具有挑战性，需要确定违反该属性的所有故障场景。这样做的规模和准确性超出了当前网络分析器的能力。在本文中，我们介绍了第一种可扩展的、准确的支持BGP、OSPF、ECMP和静态路由的概率网络配置分析器NetDice。我们的主要贡献是一个推理算法，以有效地探索故障场景的空间。更具体地说，给定一个网络配置和一个ϕ属性，我们的算法自动识别一组链路，可以证明这些链路的故障不会改变ϕ是否成立。通过修剪这些故障场景，NetDice能够精确地近似P(ϕ)。NetDice支持实用的属性和表达性故障模型，包括相关的链接故障。我们实现NetDice并在实际配置上评估它。NetDice是实用的:它可以在几分钟内精确地验证概率特性，即使在大型网络中也是如此。  

动机： (i) 现有的方法集中于验证“硬”属性，产生一个是或否的答案，以确定该属性是否适用于所有或一组固定的故障场景。除了硬属性之外，网络运营商通常还需要对“软”属性进行推理，这些属性可能会在很短的时间内被违反。在网络验证领域虽然涌现了很多关于控制平面和数据平面验证的工具，但没有一种方法可以解释网络处于给定状态的概率。 (ii) 旨在解决一个仍然悬而未决的基础研究问题:在依赖BGP和普通IGP的大型网络中，是否有可能构建一个可扩展的网络验证工具，能够精确验证概率性的属性，以支持甚至更严格的SLA(四/五个9，某属性的概率保持99.999%之类的带9的概率)？  

贡献： (i) 对网络分析的概率问题的介绍——网络验证领域的一个新方面。 (ii) 一类适用于有效概率推理的实用网络属性。 (iii) 一个可扩展的推理算法，有效地修剪BGP和普通IGPs的故障空间，以计算表达性故障模型的一个属性的概率. (iv) NetDive，对概率分析网络属性的实现，并在真实网络拓扑和配置中进行了评估。  

4. A Programmable Framework for Validating Data Planes(2018)   Abstract—Due to the emerging trend of programmable network hardware, developers have begun to explore ways to accelerate various applications and services. As a result, there is a pressing need for new tools and techniques for debugging network devices. This paper presents NetDebug, a fully programmable hardware-software framework for validating and real-time debugging of programmable data planes. We describe validation use cases, compare our design to alternative solutions, and present a preliminary evaluation using a prototype implementation.   摘要：由于可编程网络硬件的兴起，开发人员已经开始探索加速各种应用和服务的方法。因此，我们迫切需要新的工具和技术来调试网络设备。提出了一种可编程数据平面验证和实时调试的全可编程软硬件框架NetDebug。我们描述验证用例，将我们的设计与替代解决方案进行比较，并使用原型实现给出初步评估。  

动机： (i) 由于可编程数据平面的兴起，增加了对网络内计算的探讨，导致了需要新的工具来确保网络设备在完成如此多工作的同时来保持其正确性。 (ii) 当将程序移动到网络硬件时，验证软件应用程序的正确性的挑战在于(a)控制平面和数据平面的分离使得很难推断程序运行时的确切配置。(b)调试网络设备往往取决于网络流量。一旦交换机停止发送数据包，现有的工具就无法诊断错误。(c)网络编程语言，如P4，通过抽象出特定于体系结构的细节，被设计成与目标无关, 尽管这增加了代码的可移植性，但它可能会导致问题;代码在某些目标上可能有未定义的行为，并且编译器可能只支持语言规范的一个子集。  

贡献： (i) 介绍了NetDebug, 一个用于验证数据平面的可编程框架。网络调试利用P4语言和硬件设计来提供可编程网络设备的灵活性和可视性。 (ii) 已经实现了一个NetDebug原型，并使用NetDebug调试几种数据平面进行评估，能够有效的发现错误。  

5. Debugging P4 programs with Vera (2018)  

Abstract—We present Vera, a tool that verifies P4 programs using symbolic execution. Vera automatically uncovers a number of common bugs including parsing/deparsing errors, invalid memory accesses, loops and tunneling errors, among others. Vera can also be used to verify user-specified properties in a novel language we call NetCTL. To enable scalable, exhaustive verification of P4 program snapshots, Vera automatically generates all valid header layouts and uses a novel data-structure for match-action processing optimized for verification. These techniques allow Vera to scale very well: it only takes between 5s-15s to track the execution of a purely symbolic packet in the largest P4 program currently available (6KLOC) and can compute SEFL model updates in milliseconds. Vera can also explore multiple concrete dataplanes at once by allowing the programmer to insert symbolic table entries; the resulting verification highlights possible control plane errors. We have used Vera to analyze many P4 programs including the P4 tutorials, P4 programs in the research literature and the switch code from https://p4.org. Vera has found several bugs in each of them in seconds/minutes.  

摘要：我们给出了一个使用符号执行验证P4程序的工具Vera。Vera会自动发现一些常见的错误，包括解析/分离错误、无效内存访问、循环和隧道错误等。在一种我们称为NetCTL的新颖语言中，Vera还可以用来验证用户指定的属性。 为了支持P4程序快照的可扩展、详尽的验证，Vera自动生成所有有效的头布局，并使用一种新颖的数据结构进行匹配-动作处理，以进行验证优化。这些技术允许Vera很好地扩展:在目前可用的最大的P4程序(6KLOC)中，只需要5-15秒就可以跟踪一个纯符号包的执行，并且可以在毫秒内计算SEFL模型更新。通过允许程序员插入符号表项，Vera还可以同时探索多个具体的数据平面;结果验证突出了可能的控制平面错误。 我们已经使用Vera分析了许多P4程序，包括P4指南，研究文献中的P4程序和来自https://p4.org的交换机代码。Vera在几秒或几分钟内就发现了它们的多个漏洞。  

动机： (i) 调试P4程序十分困难，在传统程序中，当出现严重错误(如未映射内存访问或除零)时，硬件陷阱中断程序，调试器可以快速跟踪这些错误的来源。但在P4可编程交换机的情况下，当出现错误时，在运行时静默处理:触发错误行为的包被丢弃或以未指定的方式修改，这两种情况下，跟踪漏洞的位置都非常困难。 (ii) 如果P4要实现它的目标，即启用可编程网络来取代今天可靠的、僵化的网络，就必须要确保P4程序易于调试和修复，就需要一种可靠的用于验证P4程序的工具。  

贡献： (i) 实现了Vera，一个使用符号执行来彻底验证大型P4程序快照的工具。Vera依赖于许多创新，包括自动策略验证和新颖的匹配动作数据结构，并可以通过符号规则探索大量表快照。 (ii) 现有传统网络和SDN网络下诞生了很多数据平面或控制平面验证工具，Vera是对该工作的补充：它产生了P4程序的SEFL模型，这些模型可以用在Symnet的全网数据平面分析中。  

概述： (i) Vera使用符号执行来测试P4程序对所有可能数据包的行为。运行时，用户将P4源文件的名称和一组在程序启动时的插入表规则的命令作为参数传递。Vera首先将P4程序和提供的表规则翻译成SEFL语言，得到一个等价的程序。最终的SEFL程序是一个虚拟端口的集合，每个虚拟端口都有相关的SEFL指令。 (ii) Vera检查P4解析器状态机，并为程序可接受的每个头布局生成一个符号包;符号包中的所有字段被设置为符号值，这意味着它们接受其域中的任何值。Vera将这些数据包注入到程序的输入端口，并使用Symnet进行符号执行。 (iii) 当符号执行结束时，输出是一个包列表。对于每个数据包，我们知道它是失败还是成功，它访问的端口，它运行的指令，以及每个报头字段和元数据的状态:符号报头字段的具体值或约束。  

6. p4v: Practical Verification for Programmable Data Planes(2018)   Abstract—We present the design and implementation of p4v, a practical tool for verifying data planes described using the P4 programming language. The design of p4v is based on classic verification techniques but adds several key innovations including a novel mechanism for incorporating assumptions about the control plane and domain-specific optimizations which are needed to scale to large programs. We present case studies showing that p4v verifies important properties and finds bugs in real-world programs. We conduct experiments to quantify the scalability of p4v on a wide range of additional examples. We show that with just a few hundred lines of control-plane annotations, p4v is able to verify critical safety properties for switch.p4, a program that implements the functionality of on a modern data center switch, in under three minutes.  

摘要：本文介绍p4v的设计和实现，p4v是一种实用的工具，用于验证使用P4编程语言描述的数据平面。p4v的设计是基于经典的验证技术，但增加了几个关键的创新，包括一个新的机制，结合了关于控制平面的假设和特定领域的优化，这是扩展到大型程序所需的。我们展示了案例研究，表明p4v验证了重要的属性，并在真实的程序中发现了错误。我们进行了大量的实验来量化p4v的可扩展性。我们展示了只用几百行控制平面注释，p4v就能够在不到三分钟的时间内验证switch.p4的关键安全属性，这是一个在现代数据中心交换机上实现功能的程序。  

动机： (i) 随着可编程网络的兴起，相比于传统网络，数据平面功能不受供应商控制，可以由程序员定义，这种方法不仅促进了快速的创新，它还为网络的新用途开辟了机会，网络的可编程性带来了好处，同时也为其正确性带来了挑战。 (ii) P4是自动化验证的理想目标。传统设备的行为在很大程度上是不确定的，必须通过测试来发现，而P4数据平面以人类可读的语言对其如何处理数据包进行了精确的位级描述。通过向开发人员提供强大的、基于语言的验证工具，能够减少实践中出现的bug。  

贡献： (i) 使用真实世界的例子来激发数据平面验证的需要，并且识别了在许多P4程序中出现的公共属性的类别。 (ii) 提出了一种新的数据平面验证方法，并结合了符号化的控制平面接口。 (iii) 开发了一个原型实现和特定领域的优化，以改进原始的方法。 (iv) 通过案例研究和实验，证明了p4v能够有效地发现现实程序中的bug，并提供了良好的性能。  

概述：p4v提出用Hoare逻辑子句(前置和后置条件)来注释P4程序，以支持静态验证。方法目标是捕获许多Vera在没有任何规范的情况下自动捕获的bug，但有一个不足，即Vera目前不能完全探索switch.p4中的所有表快照。p4v要求对可能的表项进行人工规范，从而简化了验证者的工作，而且它的可伸缩性很好。缺点是，人工规范既繁琐又容易出错。  

7. Validating Datacenters At Scale(2019)   Abstract—We describe our experiences using formal methods and automated theorem proving for network operation at scale. The experiences are based on developing and applying the SecGuru and RCDC (Reality Checker for Data Centers) tools in Azure. SecGuru has been used since 2013 and thus, is arguably a pioneering industrial deployment of network verification. SecGuru is used for validating ACLs and more recently RCDC checks forwarding tables at Azure scale. A central technical angle is that we use local contracts and local checks, that can be performed at scale in parallel, and without maintaining global snapshots, to validate global properties of datacenter networks. Specifications leverage declarative encodings of configurations and automated theorem proving for validation. We describe how intent is automatically derived from network architectures and verification is incorporated as prechecks for making changes, live monitoring, and for evolving legacy policies. We document how network verification, grounded in architectural constraints, can be integral to operating a reliable cloud at scale.  

摘要：我们用形式化的方法和自动化的定理来描述我们在大规模网络操作中的经验。这些经验是基于在Azure中开发和应用SecGuru和RCDC(数据中心的实时检查器)工具。SecGuru从2013年开始使用，可以说是网络验证的工业部署的先驱。SecGuru用于验证acl，最近RCDC在Azure范围内检查转发表。一个核心的技术角度是，我们使用本地契约和本地检查来验证数据中心网络的全局属性，这些可以并行执行，无需维护全局快照。规范利用配置的声明性编码和自动定理证明进行验证。我们描述了意图是如何自动地从网络架构中派生出来的，以及验证是如何作为进行更改、实时监视和演进遗留策略的预检查合并的。我们记录了基于架构约束的网络验证是如何在大规模运行可靠云的过程中不可或缺的。  

动机： (i) 当今超大规模云数据中心的路由和网络访问限制涉及数十万个路由器和数百万个端点,而对于数据中心网络中控制路由和访问的配置的正确性验证一直是一个问题，近年来已经涌现出了通过优化数据结构解决可扩展性问题的方法，处理增量更新的方法，以及发现数据中心的结构属性（如对称性）等方法，如何捕捉意图的问题也是一个值得挖掘新方法的领域。   贡献： (i) 自动意图提取:本文描述了一种方法，用于从包含拓扑和地址局部性的架构元数据中自动导出结构化数据中心网络的意图。 (ii) 局部验证:一种将端到端可达性不变量分解为一组局部契约的新技术。 (iii) 设计和实施工业部署，用于持续验证超大规模网络的路由和网络访问限制。 (iv) 从管理转发策略和网络访问控制的一组用例中描述经验。已经部署该技术来实时监控生产状态，并作为预检查来确保变更的影响符合意图。  

8.A General Approach to Network Configuration Verification (2017)  

Abstract—We present Minesweeper, a tool to verify that a network satisfies a wide range of intended properties such as reachability or isolation among nodes, way pointing, black holes, bounded path length, load-balancing, functional equivalence of two routers, and fault-tolerance. Minesweeper translates network configuration files into a logical formula that captures the stable states to which the network forwarding will converge as a result of interactions between routing protocols such as OSPF, BGP and static routes. It then combines the formula with constraints that describe the intended property. If the combined formula is satisfiable, there exists a stable state of the network in which the property does not hold. Otherwise, no stable state (if any) violates the property. We used Minesweeper to check four properties of 152 real networks from a large cloud provider. We found 120 violations, some of which are potentially serious security vulnerabilities. We also evaluated Minesweeper on synthetic benchmarks, and found that it can verify rich properties for networks with hundreds of routers in under five minutes. This performance is due to a suite of model-slicing and hoisting optimizations that we developed, which reduce runtime by over 460x for large networks.  

摘要：我们提出了一个验证网络满足广泛的预期属性（如节点间的可达性或隔离性、途经点、黑洞、限制路径长度、负载均衡、路由间的功能等价和故障容忍）的工具，Minesweeper。Minesweeper将网络配置文件转换成一个逻辑公式，捕获网络转发将收敛到的稳定状态，将之作为路由协议（如OSPF、BGP和静态路由）之间交互的结果。然后，它将公式与描述预期属性的约束结合起来。如果组合公式是可满足的，则网络存在一个不支持该性质的稳定状态。否则，任何稳定状态都不会违反该属性。我们使用Minesweeper验证来自大型云提供商的152个真实网络的四个属性。我们发现了120个违规行为，其中一些是潜在的严重安全漏洞。我们还在合成基准上评估Minesweeper，发现它可以在五分钟内验证具有数百个路由器的网络的丰富属性。这种优越性能是因为我们进行了模型切片和提升的优化，使对大型网络的运行时间减少了460倍以上。  

动机： (i) 控制平面配置困难：传统的控制平面网络是一个复杂的分布式系统，网络上的设备用多个协议根据拓扑结构等来交换信息。这些设备根据它们的本地配置文件来处理信息和选择路径，文件有数千行低级指令。同时，链路错误常见并且路由器错误可能发生。 (ii) 当前不存在既能实现高网络设计覆盖率和数据平面覆盖率，又能保持足够的可扩展性，以实现许多真实网络的验证工具。  

贡献： (i) 提出一个通用的、网络控制平面和数据平面的符号模型，该模型将网络的稳定状态编码为满足SMT公式的分配。 (ii) 通过这个模型，介绍了验证广泛属性的方法，这些属性适用于所有可能出现在给定控制平面上的数据包和所有可能的数据平面。 (iii) 将该模型和验证方法在Minesweeper中实现，实验表明，Minesweeper在真实配置中查找问题是有效的，并可扩展到大型网络。   不足： Minesweeper基于SMT进行验证，通用性满足但是性能上欠缺。因为Minesweeper为提供广泛的网络设计覆盖会导致很大的搜索空间，它会验证SMT模型上所有策略。为验证k链路故障，Minesweeper最坏情况下会列举k链路故障下所有可能组合。  

9.Fast Control Plane Analysis Using an Abstract Representation (2016)  

Abstract—Networks employ complex, and hence error-prone, routing control plane configurations. In many cases, the impact of errors manifests only under failures and leads to devastating effects. Thus, it is important to proactively verify control plane behavior under arbitrary link failures. State-of-the-art verifiers are either too slow or impractical to use for such verification tasks. In this paper we propose a new high level abstraction for control planes, ARC, that supports fast control plane analyses under arbitrary failures. ARC can check key invariants without generating the data plane—which is the main reason for current tools’ ineffectiveness. This is possible because of the nature of verification tasks and the constrained nature of control plane designs in networks today. We develop algorithms to derive a network’s ARC from its configuration files. Our evaluation over 314 networks shows that ARC computation is quick, and that ARC can verify key invariants in under 1s in most cases, which is orders-of-magnitude faster than the state-of-the-art.  

摘要：网络采用复杂且容易出错的路由控制平面配置。在许多情况下，错误的影响只有在出现故障的情况下才会显现出来，并导致毁灭性的后果。因此，主动验证任意链路故障下的控制平面行为是非常重要的。最先进的验证程序要么太慢，要么不实用，不能用于此类验证任务。本文提出了一种新的控制平面的高级抽象，ARC。它支持任意故障下的快速控制平面分析。ARC可以在不生成数据平面的情况下检查键不变量，这也是目前工具失效的主要原因，而该原因可能是现在网络验证任务性质和控制平面设计的约束性质造成的。我们开发算法，从网络配置文件中生成ARC。我们对314个网络的评估表明，ARC计算速度很快，在大多数情况下，ARC可以在1以内验证关键不变量，这比最先进的算法快了几个数量级。  

动机： (i) 网络配置复杂，路由控制平面配置容易出错。 (ii) 许多配置错误的影响在出现故障后显现，且影响十分严重。   贡献： (i) 提出了ARC，一个新的路由控制平面的高级抽象，可以在任意故障场景下快速验证关键属性。 (ii) 通过ARC，将对策略的验证转化为对图属性的检查。 (iii) 对ARC进行实现，结果表明，在真实数据中心配置中ARC展现了比现有验证工具快数量级的性能。  

不足： ARC利用图算法具有了很好的性能，但是不通用，即ARC模型不包括：一些常见的三层协议（如iBGP）、二层原语（如VLANs）和一些协议属性（如BGP community）。   ARC工作工程： 包括ARC的生成和使用两个部分，其中核心为ARC的生成。 生成：ARC由一系列与路由协议无关的有向加权图组成，其生成重点是如何构建在一些限制下可证明的路径等效图，其主要问题是确定用于构建图合适的顶点、边和权重以使图是路径集等效和路径等效的。本文的很大部分工作是通过利用扩展拓扑图和算法来解决上面的问题。 使用：ARC能检查任意故障下的不变量，尤其适合验证与路径相关的不变量，因为可以将验证转化为证明扩展拓扑图的属性。即使是等效测试也是采用基于扩展拓扑图的变换，验证和等效测试的本质上都是计算图的属性的。  

CoNEXT 1.P-Rex: Fast Verification of MPLS Networks with Multiple Link Failures(2018)  

Abstract—Future communication networks are expected to be highly automated, disburdening human operators of their most complex tasks. However, while first powerful and automated network analysis tools are emerging, existing tools provide only limited (and inefficient) support of reasoning about failure scenarios. We present P-Rex, a fast what-if analysis tool, that allows us to test important reachability and policy-compliance properties even under an arbitrary number of failures, in polynomial-time, i.e., without enumerating all failure scenarios (the usual approach today, if supported at all). P-Rex targets networks based on Multiprotocol Label Switching (MPLS) and its Segment Routing (SR) extension and comes with an expressive query language based on regular expressions. It takes into account the actual router tables, and is hence well-suited for debugging. We also report on an industrial case study and demonstrate that P-Rex supports rich queries, performing what-if analyses in less than 70 minutes in most cases, in a 24-router network with over 100,000 MPLS forwarding rules.  

摘要：未来的通信网络有望实现高度自动化，从而使人类操作员无需承担最复杂的任务。但是，尽管出现了第一个功能强大且自动化的网络分析工具，但现有工具仅提供有限（且效率低下）的故障场景推理支持。我们介绍了P-Rex，一种快速的假设分析工具，它使我们能够在多项式时间内，在任意数量的故障下，也可以测试重要的可及性和策略遵从属性，即无需枚举所有故障场景（通常的方法）。 P-Rex针对基于多协议标签交换（MPLS）及其网段路由（SR）扩展的网络，并提供了基于正则表达式的表达性查询语言。它考虑了实际的路由器表，因此非常适合调试。我们还报告了一个工业案例研究，并证明了P-Rex支持丰富的查询，在大多数情况下，在具有100,000多个MPLS转发规则的24路由器网络中，执行假设分析的时间少于70分钟。  

动机： 自动化验证网络已经成为当今的趋势，但是对于计算机而言，验证网络配置仍然是一项复杂的任务，特别是在网络故障下推理网络行为。现在支持what-if分析的验证方法存在明显的缺点：因为要列举所有的故障情况，引入了组合复杂性，使得验证效率很低。   贡献： (i)论问提出了能够快速验证MPLS通信网络的验证工具P-Rex，它是一种what-if工具，考虑发生故障的可能性，P-Rex的验证与故障数量无关，在多项式时间内测试重要的网络属性，如waypoint enforcement、load-balancing、Segment Routing。 (ii)提出了基于正则表达式的查询语言，用于指定数据包的头部和路径。 (iii)提出了过度逼近和欠逼近技术，进一步提高性能。  

实验结果： (i)P-Rex可以在一个小时内完成查询10万多个转发表。相比HSA，可以找到更多的路由器连接性质。 (ii)P-Rex可以回答有关数据包在路由器传播细节的复杂的网络问题。  

2. AalWiNes: A Fast and Quantitative What-If Analysis Tool for MPLS Networks(2020)       

Abstract—We present an automated what-if analysis tool AalWiNes for MPLS networks which allows us to verify both logical properties (e.g., related to the policy compliance) as well as quantitative properties (e.g., concerning the latency) under multiple link failures. Our tool relies on weighted pushdown automata, a quantitative extension of classic automata theory, and takes into account the actual dataplane configuration, rendering it especially useful for debugging. In particular, our tool collects the different router forwarding tables and then builds a pushdown system, on which quantitative reachability is performed based on an expressive query language. Our experiments show that our tool outperforms stateof-the-art approaches (which until now have been restricted to logical properties) by several orders of magnitude; furthermore, our quantitative extension only entails a moderate overhead in terms of runtime. The tool comes with a platform-independent user interface and is publicly available as open-source, together with all other experimental artefacts.  

摘要：我们提供了一种用于MPLS网络的自动假设分析工具AalWiNes，该工具可以验证多个链路故障下的逻辑属性（例如，与策略合规性相关）以及定量属性（例如，与时延相关）。我们的工具依赖于加权下推自动机，这是经典自动机理论的定量扩展，并考虑了实际的数据平面配置，从而使其对于调试特别有用。我们的工具收集了不同的路由器转发表，然后构建了下推式系统，在该系统上，基于表达性查询语言执行了定量可达性。我们的实验表明，我们的工具比最先进的方法（迄今为止仅限于逻辑属性）要好几个数量级。此外，我们的定量扩展仅在运行时方面需要适度的开销。该工具带有与平台无关的用户界面，并且与所有其他实验人工制品一起以开源形式公开提供。   动机： 网络中单条路径的故障就会引发很多意外的网络行为，仅保证故障下网络行为的逻辑正确性（如策略合规性）通常是不够的，一个可靠的网络还需要满足定量特性，即使存在一定数量的故障，也存在一条短路径可以重新路由。  

贡献： (i)提出了能够在故障情况下验证MPLS通信网络的what-if工具AalWiNes，AalWiNes依靠一种表达性查询语言测试逻辑属性（策略合规性等）和定量属性（延迟、跳数、所需的标签堆栈大小），在多项式时间内使用过度逼近和欠逼近技术处理任意数量的链接失败。 (ii)提出了加权下推自动机，并提出了新颖的算法，进行定量可达性分析。 系统结构： Moped Binary      图9 系统结构图 如图9所示，AalWiNes通过GUI获得路由转发表的数据平面快照，如果网络配置发生变化，则需要获取新的数据平面快照。图形用户界面可以加载MPLS网络，查询以及表现可能的权重表达式。然后，AalWiNes通过过度逼近来构造下推式自动机，再通过删除冗余规则以减小其大小，对构造的（加权的）下推自动机执行一系列的缩减（基于静态分析），然后将减少的下推发送到Moped引擎(仅在未指定重量要求的情况下才可能）或发送到接受加权和未加权下推自动机的求解器。如果验证结果表明不满足查询条件，将得出结论性答案并将其报告给GUI。 否则，AalWiNes将构造一个近似逼近的下推自动机，在其中添加一个全局故障链接计数器，并使用此计数器来确保不超过故障链接的总数。  

3. Detecting Routing Loops in the Data Plane(2020)  

Abstract—Routing loops can harm network operation. Existing loop detection mechanisms, including mirroring packets, storing state on switches, or encoding the path onto packets, impose significant overheads on either the switches or the network. We present Unroller, a solution that enables real-time identification of routing loops in the data plane with minimal overheads. Our algorithms encode a varying fixed-size subset of the traversed path on each packet. That way, our overhead is independent of the path length, while we can detect the loop once the packet returns to some encoded switch. We implemented Unroller in P4 and compiled into three different FPGA targets. We then compared it against state-of-the-art solutions on real WAN and data center topologies and show that it requires from 6x to 100x fewer bits added to packets than existing methods.  

摘要：路由环路可能会损害网络运行。现有的环路检测机制（如镜像数据包将状态存储在交换机上或将路径编码到数据包上）给交换机或网络带来了巨大的开销。 我们介绍了Unroller这解决方案，可以以最小的开销实时识别数据平面中的路由环路。我们的算法对每个数据包中遍历路径的变化的固定大小子集进行编码。 因此，我们的开销与路径长度无关，一旦数据包返回到某个编码的交换机，我们就可以检测到环路。我们在P4中实现了Unroller，并将其编译为三个不同的FPGA目标。我们将其与实际WAN和数据中心拓扑上的最新解决方案进行了比较，结果表明，与现有方法相比，它向数据包添加的比特数减少了6到100倍。  

动机：        路由环路是路由不稳定的主要原因之一，会损害网络的性能，现有的环路检测机制给交换机网络带来了巨大的开销。环路检测的高级方法有在交换机上存储状态和镜像选定的数据包头部，前者导致交换机的大量开销，后者导致网络的显著开销。  

贡献： (i)提出了Unroller,通过在数据包上存储信息，可以实时识别数据平面中的路由环路。 (ii)在P4上实现了论文的思想，并将其编译为三个不同的FPGA目标 开源代码：https：//github.com/kucejan/unroller  

实验结果：        论文将Unroller与WAN和数据中心拓扑上的最新解决方案进行了比较，结果表明，与现有方法相比，Unroller向数据包添加的比特数减少了6到100倍。Unroller在应用阈值技术的时候，假阳性会随着阈值大小成倍减小。

  INFOCOM

1. Efficient Network Configuration Verification Using Optimized Datalog (2018)   Abstract—Network correctness and reliability are often the greatest concerns. Users use low-level configurations to realize sophisticated policies, particularly in enterprise and datacenter network, which inevitably makes errors. Existing solutions that verify whether the configuration satisfies intended policies either suffer hardcode models, absence of specification languages or scale poorly. In this paper, we propose a new framework, BEEP, which has a high-level specification and modeling language. BEEP takes configuration files as inputs, models control plane via a compact way of sharing information, and then verifies using optimized Datalog rules/quires. Finally, it either indicates success or returns counterexamples that help to debug the configuration.  

摘要：网络的正确性和可靠性通常是最重要的。用户使用低级配置来实现复杂的策略，特别是在企业和数据中心网络中，不可避免地会出现错误。验证配置是否满足预期策略的现有解决方案要么受到硬代码模型的影响，要么缺乏规范语言，要么伸缩性差。本文提出了一个新的框架BEEP，它具有高级的规范和建模语言。BEEP以配置文件为输入，通过共享信息的紧凑方式对控制平面进行建模，然后使用优化的数据记录规则/查询进行验证。最后，它要么表明成功，要么返回帮助调试配置的反例。  

动机： (i) 由于低级配置语言和高级网络策略的差异，以及路由协议及其交互的复杂性，更深层次的验证策略无法准确表达，配置错误是不可避免的。 (ii) 现有的验证工具如，Batfish, ERA等，是控制平面模型是硬编码的，并且缺乏规范语言以及伸缩性。  

贡献： (i) BEEP基于Datalog开发，Datalog支持定义、递归和分层否定。因此BEEP可以表达更深层次的验证策略，例如，跨多个路径的可达性差异。同时也支持bit的重写。 (ii) BEEP可以计算所有的解。大多数经典的验证工具(SMT求解器)只提供单一的解，例如，对于可达性策略，可以找到从主机A到主机B的所有数据包头。(iii)依托优化的数据结构(表结构为BDD)和算法，BEEP具有良好的可伸缩性。   BEEP工作过程： 图10 BEEP的工作过程  

HotNets

1. Putting network verification to good use (2019)  

Abstract—The past decade has witnessed remarkable progress in the field of network verification, and interest from academia and industry has spurred the development of increasingly sophisticated verification tools and algorithms. However, outside of a handful of large cloud computing providers, the use of network verification is still sparse. We argue that the next frontier for network verification is to enable easy and effective use by "average" network engineers. Whereas in software development, practitioners frequently use testing frameworks to describe the expected behavior of their systems and to measure the effectiveness of their tests through metrics such as code coverage, no such frameworks exist for the equally challenging task of designing and maintaining networks. To address this gap, we outline the design of a network verification framework. In doing so, we propose 1) a method to compute test coverage for networks, which tells engineers how well their invariants are testing the network; and 2) a new declarative invariant language that makes it easy to express network invariants and enables computation of coverage metrics.  

摘要：近年来，网络验证领域取得了长足的发展，学术界和工业界对网络验证工具和算法的研究兴趣日益浓厚。然而，除了少数大型云计算提供商之外，网络验证的使用仍然很少。我们网络验证的下一个前沿是使“普通”网络工程师能够轻松有效地使用。在软件开发中，实践者经常使用测试框架来描述系统的预期行为，并通过诸如代码覆盖率之类的指标来衡量测试的有效性，但对于设计和维护网络这样具有同等挑战性的任务，没有这样的框架存在。为了解决这个差距，我们概述了一个网络验证框架的设计。为此，我们提出了1)一种计算网络测试覆盖的方法，它告诉工程师他们的不变量测试网络的效果如何; 2)一种新的声明性不变量语言，使表达网络不变量变得容易，并支持覆盖率度量的计算。   系统结构： 图11 系统结构 动机： (i) 验证工具没有普遍使用。虽然目前已经有了许多验证工具，如HAS、VeriFlow、Batfish、ARC等。但是除了少数规模较大的组织外，这些验证工具并没有得到普遍使用。并且，验证工具的前景应是简单高效，而不是更加复杂。 (ii) 现有的验证工具不能指导用户了解他们的测试结果有多“好”，或者网络的哪些方面还没有测试。 (iii) 网络验证使用不充分。在进行了网络验证以后，网络在运行过程中依然会发生中断，是因为网络不变量等一些关键因素没有被测试。  

贡献： (i)  提出了一个新的网络测试框架的设计(图11)，形式化了网络覆盖的定义，并提出计算网络测试覆盖率的方法。通过网络测试覆盖率，用户可以知道网络每个部分的测试结果。 (ii) 提出一种新的声明性不变量语言，使表达网络不变量变得容易，并支持覆盖率度量的计算。 (iii) 提出的架构以及声明性不变量语言简化了网络测试的编写，使得普通网络运营商更容易获得该验证工具。    

2. Incremental Network Configuration Verification (2020)   Abstract—Network configurations are constantly changing, and each change poses a risk of catastrophic network outages. Consequently, the net- working community has put significant effort into developing and optimizing configuration verifiers. However, we observe existing configuration verifiers still have a significant drawback: they are not optimized for configuration changes. That is, they always check a snapshot of network configuration from scratch, even though the configuration often changes slightly since the last verification. In this paper, we demonstrate the benefits, opportunities, and challenges of incremental network configuration verification (INCV). We also demonstrate the feasibility of INCV by introducing RealConfig, an incremental configuration verifier that can check configuration changes within one second.

摘要：网络配置是不断变化的，每一次变化都有可能导致灾难性的网络中断。因此，网络工作社区投入了大量的精力来开发和优化配置验证器。然而，我们观察到现有的配置验证器仍然有一个显著的缺点:它们没有针对配置更改进行优化。也就是说，他们总是从头开始检查网络配置的快照，即使在最后一次验证之后，配置常常会略有变化。在本文中，我们论证了增量式网络配置验证(Incremental Network Configuration Verification, INCV)的好处、机会和挑战。我们还通过引入RealConfig来演示INCV的可行性，RealConfig是一个增量配置验证器，可以在一秒内检查配置更改。   动机： (i) 现有的配置验证工具都有一个严重的缺点：没有针对配置更改进行优化。即使配置只有细微的更改，也可能无法满足基本的策略需求。当面临大规模的配置更改时，更是一个困难、耗时的问题。 (ii) 能否利用之前验证过程的内部状态和结果来显著加快配置更改的验证? (iii) 由于可伸缩性原因，现有配置验证程序没有对底层协议消息建模，因此不能利用协议内置的信令机制来确定配置更改后的哪个路由/转发状态仍然有效。 (iv) 长时间运行的网络可能包含非常复杂的配置，并且由不同的运营商更新。随着时间的推移，越来越难确定运营商想要什么样的网络行为，导致网络规范挖掘困难，准确度下降。此外，当前的规范挖掘方法需要检查所有可能的策略，通常需要非常长的时间。  

贡献： (i)  提出了RealConfig(图12)来实现INCV，RealConfig通过(部分)重用先前验证过程的内部状态和结果来进行增量式网络配置验证，并证明其可行性。RealConfig拥有三个部分，每个部分都支持增量操作。RealConfig使用Differential Datalog来实现增量转发规则计算(第1部分)；使用修改版的APkeep进行模型更新(第二部分)；RealConfig通过跟踪等价类与节点和转发路径之间的映射关系，识别出所有受影响的路径，并根据它们新的转发行为修改这些路径并输出(第三部分)。 (ii)根据实验结果， INCV可以将数据平面计算时间提高20 ~ 92倍。   RealConfig的工作流程： 图12 RealConfig的工作流程