ACORN：使用路由不确定性的网络控制平面抽象
ACORN: Network Control Plane Abstraction using Route Nondeterminism
摘要：
网络很难正确配置，并且经常发生错误配置，导致中断或安全漏洞。形式化验证技术被应用于保证网络配置的正确性，从而提高网络的可靠性。这项工作解决了分布式网络控制平面的验证，有两个不同的贡献，以提高形式化验证的可扩展性。我们的第一个贡献是一个层次的抽象不同的精度，引入不确定性的路由选择过程中，路由器用来选择最佳的可用路由。我们证明了这些抽象的合理性，并显示其好处。我们的第二个贡献是一种新的SMT编码，它使用符号图编码所有可能的稳定的路由树，符合给定的网络控制平面配置。我们已经实现了我们的抽象和SMT编码的原型工具称为ACORN。我们的评估表明，我们的抽象可以提供显着的相对加速（高达323倍）的性能，和ACORN可以扩展到$\approx37,000$路由器（组织在FatTree拓扑结构，合成最短路径路由和无谷策略）验证可达性。这远远超过了用于控制平面验证的现有工具的性能。
英文摘要：
Networks are hard to configure correctly, and misconfigurations occur frequently, leading to outages or security breaches. Formal verification techniques have been applied to guarantee the correctness of network configurations, thereby improving network reliability. This work addresses verification of distributed network control planes, with two distinct contributions to improve the scalability of formal verification. Our first contribution is a hierarchy of abstractions of varying precision which introduce nondeterminism into the route selection procedure that routers use to select the best available route. We prove the soundness of these abstractions and show their benefits. Our second contribution is a novel SMT encoding which uses symbolic graphs to encode all possible stable routing trees that are compliant with the given network control plane configurations. We have implemented our abstractions and SMT encodings in a prototype tool called ACORN. Our evaluations show that our abstractions can provide significant relative speedups (up to 323x) in performance, and ACORN can scale up to $\approx37,000$ routers (organized in FatTree topologies, with synthesized shortest-path routing and valley-free policies) for verifying reachability. This far exceeds the performance of existing tools for control plane verification.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
