FLash-3

Flash-解决更新风暴、长尾到达的最新数据平面验证-学习4

相关工作

大规模网络的网络验证。
<1>由于其重要性，各种研究已经对大规模网络的网络验证进行了研究。
<2>一些设计侧重于控制平面，这与Flash所关注的数据平面验证是互补的，而一些设计仅适用于特定的网络结构和特定的需求，而Flash针对的是更通用的网络和需求。
<3>Libra提出通过分布式计算来扩展大规模网络的验证。它将头部空间划分为最小的原子子空间，其中每个子空间必须具有相同的转发行为，并且本质上是Flash中的等价类，并将这些子空间的验证分发给一组验证器。
<4>Flash中子空间划分的设计是受Libra的启发。然而，Flash中子空间分区的主要目的是减少FIB更新的排队和内存成本。因此，Flash允许在一个子空间中验证多个EC
<5>一些大型网络使用基于仿真的控制平面验证工具。Flash可以通过验证生成的规则来很好地补充这些研究。最近的研究是这一方向的先驱。

数据平面验证。
<1>数据平面表示是数据平面验证的核心数据结构。一些数据平面验证工具使用流表(SDN)表示，并在此基础上开发计算模型（例如，SAT模型[17]、头部空间代数和分组转换函数[18]以及数据日志模型[27]）。
<2>另一组数据平面验证工具使用等效类作为数据平面表示。等价类将头部空间分析和需求验证解耦，如果EC的数量较少，这两个步骤都可以有效地执行。
<3>最近的研究也通过维护多组EC和延迟计算叉积来缓解EC的爆炸。
<4>EC方法还受益于有效的数据结构来操作头部空间：Delta-net[25]开发了一种基于间隔的数据结构，该结构在处理基于前缀的规则时是有效的，而其他方法（例如，APKeep[26]和Flash）在更通用的设置下使用二进制决策图（BDD）来提高内存效率。
<5>在EC方法中，Flash是第一个设计高效数据结构来存储和操作操作的方法，只有在应用于大规模网络时，这一点才变得至关重要。
<6>DNA[47]还独立开发了两种批量更新的想法。具体而言，“批量插入和删除”的想法与“删除取消更新”（算法1中的L1）相同，“同一设备上的批量转发行为”的想法类似于Flash中的“按操作聚合”（Reduce I），但限制更大：聚合的更新在更新前后必须具有相同的操作。
<7>随着Flash对块更新问题进行了更深入的分析，Fast IMT中开发的优化是通用的，可以应用于其他EC实现。

网络中的自动机理论。
<1>递减验证图的想法是由将自动机理论应用于策略路由的研究推动的。这些研究将网络和路由约束建模为自动化。通过计算乘积自动机，这些研究可以识别满足路由约束的网络路径。
<2>Flash也计算乘积自动机，但将其用于验证目的，并结合最近的快速可达性检查方法[41]。

讨论

作者Flash可能扩展的三个方面：需求规范、数据平面模型和实现。

需求规范。
<1>目前，Flash使用路径正则表达式（PRE）来表达需求规范。虽然PRE简单易懂，但它通常需要最短路径等假设来避免状态爆炸，并且不能轻易扩展以支持非最短路径算法。
<2>由于Flash使用需求规范来构建对所有有效路径进行编码的递减验证图（DVG），因此一个潜在的扩展是直接将DVG作为输入。
<3>因此，Flash可能与许多SDN编程语言（例如[42，43，55-59]）的前端接口，这些语言也计算所有有效路径的集合。

数据平面模型。
<1>Flash专注于数据平面模型，在该模型中，数据包仅基于报头转发，不存在报头重写，因为与运营商的讨论表明，报头重写大多发生在我们目标大规模网络中的终端主机（例如[60]）。
<2>然而，可能需要将Flash扩展到有状态路由（例如，P4[61]和NPL[62]），或者支持常见的报头重写，例如NAT或隧道。
<3>状态路由需要扩展到快速IMT。具体而言，转发功能模型b(ℎ) 需要修改为b(ℎ,s),其中s表示状态。
<4>如果这些操作可能会更改标头或状态，则需要扩展到CE2D。有两个方向可以处理Flash中的头/状态重写。
<5>第一个方向（例如，[26]）是保证任何数据包，如果被重写，在重写之前和之后都属于精确的一个EC。
<6>另一个方向是启用递归查询（例如，[54]）。
<7>必须扩展CE2D，例如，通过在不同EC的递减验证图之间添加链接。当可以在不同步的节点上执行报头重写时，随着不确定性的增加，CE2D的好处可能会减少。这两种方法都可以破坏子空间分区，因为头重写后的EC可能属于另一个分区，甚至属于另一台机器。

实施
<1>Flash已经提供了许多优化。进一步提高Flash性能优势的一个潜在扩展是利用并行性和管道技术。
<2>目前，子空间验证器的快速IMT和CE2D在同一核心上运行。有了更多的CPU，我们可以将这两个步骤解耦，并并行化每个EC的需求验证。
<3>快速IMT也可以通过利用最近的BDD库（例如[63]）来并行化，这些库允许高效的并发BDD/谓词操作。

总结

<1>作者设计了Flash，这是一个快速且可扩展的系统，它解决了大规模网络数据平面验证中的两个重要问题：更新风暴和长尾更新到达。
<2>Flash提出了两个新想法：通过优化块更新处理实现快速逆模型转换，以及通过部分完整的数据平面信息实现一致验证的一致、高效、早期检测。
<3>在大规模数据集上进行的大量实验证明了其有效性和效率。

附录

转发模型（基于规则的表示）：三部分：匹配断言r.pred∈P，优先级r.pr∈N，输出向量(r,y) -> 模拟FIB转发
逆模型（基于等价类的表示）：每个逆模型是一组(p,y)对，其中p∈P是断言，y∈Y是输出向量。显然，模型的空间是P×Y的子集。然而，逆模型必须满足约束条件，如定义6所示。我们定义了一个布尔函数im，它取P×Y的子集，如果它是逆模型，则返回1，否则返回0。

赏

×

纯属好玩

扫码打赏，你说多少就多少

打开支付宝扫一扫，即可进行扫码打赏哦