Current network control plane verification tools cannot scale to large networks, because of the complexity of jointly reasoning about the behaviors of all nodes in the network. In this paper we present a modular approach to control plane verification, whereby end-to-end network properties are verified via a set of purely local checks on individual nodes and edges. The approach targets the verification of safety properties for BGP configurations and provides guarantees in the face of both arbitrary external route announcements from neighbors and arbitrary node/link failures. We have proven the approach correct and also implemented it in a tool called Lightyear. Experimental results show that Lightyear scales dramatically better than prior control plane verifiers. Further, we have used Lightyear to verify three properties of the wide area network of a major cloud provider, containing hundreds of routers and tens of thousands of edges. To our knowledge no prior tool has been demonstrated to provide such guarantees at that scale. Finally, in addition to the scaling benefits, our modular approach to verification makes it easy to localize the causes of configuration errors and to support incremental re-verification as configurations are updated.

翻译：当前网络控制平面验证工具无法扩展到大规模网络，原因在于联合推理网络中所有节点行为的复杂性。本文提出一种模块化控制平面验证方法，通过一组对单个节点和边的纯局部检查来验证端到端网络属性。该方法针对BGP配置的安全属性验证，在邻居任意外部路由通告以及任意节点/链路故障场景下均能提供保障。我们已证明该方法的正确性，并在名为Lightyear的工具中实现。实验结果表明，Lightyear的可扩展性显著优于先前的控制平面验证器。此外，我们使用Lightyear验证了一家主要云服务提供商广域网的三个属性，该网络包含数百个路由器和数万条边。据我们所知，尚无先前的工具能在该规模下提供此类保障。最后，除扩展性优势外，我们的模块化验证方法还能轻松定位配置错误原因，并支持配置更新时的增量式重新验证。