一种精确表达的格理论网络验证框架
A Precise and Expressive Lattice-theoretical Framework for Efficient Network Verification
摘要：
网络验证承诺通过逻辑分析控制或数据平面来检测错误，例如黑洞和转发循环。为了有效地这样做，最先进的技术（例如，Veriflow）将具有相同转发行为的数据包报头划分为相同的数据包等价类（PEC）。最近，Yang和Lam展示了如何构造PEC的最小集合，称为原子谓词。它们的构造使用二元决策图（BDD）。然而，BDD已被证明会导致每个数据包报头位的显着开销，在分析大规模数据中心时表现不佳。原子谓词的开销促使ddNF设计了一种专用的三进制位向量（TBV）数据结构。然而，TBV的表达严格低于BDD。此外，与原子谓词不同，ddNF的PEC集不是最小的。我们表明，ddNF的非极小是由于空PEC。此外，显示空PEC会触发错误的分析结果。这揭示了在正式网络验证中精确度、表现力和性能之间的内在紧张关系。我们的论文通过一种新的格理论PEC构造算法#PEC解决了这种紧张局势，该算法如下所述地推进了该领域：（i）#PEC可以编码更多种类的转发规则（例如，ip-tables），（ii）#PEC验证更宽类别的错误（例如，阴影规则）比ddNF，以及（iii）在广泛的真实世界数据集上，#PEC比原子谓词快10倍。通过实现精度，表现力和性能，本文回答了一个长期的追求，跨越了三代正式的网络分析技术。
英文摘要：
Network verification promises to detect errors, such as black holes and forwarding loops, by logically analyzing the control or data plane. To do so efficiently, the state-of-the-art (e.g., Veriflow) partitions packet headers with identical forwarding behavior into the same packet equivalence class (PEC). Recently, Yang and Lam showed how to construct the minimal set of PECs, called atomic predicates. Their construction uses Binary Decision Diagrams (BDDs). However, BDDs have been shown to incur significant overhead per packet header bit, performing poorly when analyzing large-scale data centers. The overhead of atomic predicates prompted ddNF to devise a specialized data structure of Ternary Bit Vectors (TBV) instead. However, TBVs are strictly less expressive than BDDs. Moreover, unlike atomic predicates, ddNF's set of PECs is not minimal. We show that ddNF's non-minimality is due to empty PECs. In addition, empty PECs are shown to trigger wrong analysis results. This reveals an inherent tension between precision, expressiveness and performance in formal network verification. Our paper resolves this tension through a new lattice-theoretical PEC-construction algorithm, #PEC, that advances the field as follows: (i) #PEC can encode more kinds of forwarding rules (e.g., ip-tables) than ddNF and Veriflow, (ii) #PEC verifies a wider class of errors (e.g., shadowed rules) than ddNF, and (iii) on a broad range of real-world datasets, #PEC is 10X faster than atomic predicates. By achieving precision, expressiveness and performance, this paper answers a longstanding quest that has spanned three generations of formal network analysis techniques.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
