Monolithic control plane verification cannot scale to hyperscale network architectures with tens of thousands of nodes, heterogeneous network policies and thousands of network changes a day. Instead, modular verification offers improved scalability, reasoning over diverse behaviors, and robustness following policy updates. We introduce Timepiece, a new modular control plane verification system. While one class of verifiers, starting with Minesweeper, were based on analysis of stable paths, we show that such models, when deployed naively for modular verification, are unsound. To rectify the situation, we adopt a routing model based around a logical notion of time and develop a sound, expressive, and scalable verification engine. Our system requires that a user specifies interfaces between module components. We develop methods for defining these interfaces using predicates inspired by temporal logic, and show how to use those interfaces to verify a range of network-wide properties such as reachability or access control. Verifying a prefix-filtering policy using a non-modular verification engine times out on an 80-node fattree network after 2 hours. However, Timepiece verifies a 2,000-node fattree in 2.37 minutes on a 96-core virtual machine. Modular verification of individual routers is embarrassingly parallel and completes in seconds, which allows verification to scale beyond non-modular engines, while still allowing the full power of SMT-based symbolic reasoning.

翻译：单体控制平面验证无法扩展到拥有数万个节点、异构网络策略以及每天数千次网络变更的超大规模网络架构。相比之下，模块化验证提供了更好的可扩展性、对多样化行为的推理能力以及策略更新后的鲁棒性。我们提出了 Timepiece，一种新型模块化控制平面验证系统。虽然以 Minesweeper 为首的一类验证器基于稳定路径分析，但我们表明，这类模型在直接用于模块化验证时是不正确的。为纠正这一问题，我们采用了一种基于逻辑时间概念的选路模型，并开发了一个正确、表达力强且可扩展的验证引擎。该系统要求用户指定模块组件之间的接口。我们开发了使用受时序逻辑启发的谓词来定义这些接口的方法，并展示了如何利用这些接口验证一系列网络级属性，如可达性或访问控制。使用非模块化验证引擎验证一个前缀过滤策略时，在80节点胖树网络上运行2小时后超时。然而，Timepiece 在96核虚拟机上仅用2.37分钟即可验证一个2000节点的胖树网络。对单个路由器的模块化验证具有令人尴尬的并行性，并在数秒内完成，这使得验证能够超越非模块化引擎的规模限制，同时仍保留基于SMT符号推理的全部能力。