一句话：提出 Timepiece，用逻辑时间路由模型与受时序逻辑启发的接口谓词，实现可靠可扩展的模块化控制平面验证。
单体控制平面验证难以扩展到数万节点、异构策略且日变更频繁的网络；模块化验证可提升扩展性，但直接套用稳定路径模型并不可靠。本文提出 Timepiece，采用基于逻辑时间的路由模型，并要求用户用受时序逻辑启发的谓词指定模块接口。基于这些接口，系统构建可靠、表达力强且可扩展的验证引擎，支持可达性、访问控制等全网性质验证，并保留 SMT 符号推理能力。评估中，非模块化引擎验证 80 节点 fattree 的 prefix-filtering 策略 2 小时后超时；Timepiece 在 96 核虚拟机上 2.37 分钟验证 2000 节点 fattree，单路由器模块化验证可并行完成，仅需数秒。
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 naïvely 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.
@article{paperbot2006,
title = {Modular Control Plane Verification via Temporal Invariants},
author = {Timothy Alberdingk Thijm and Ryan Beckett and Aarti Gupta and David Walker},
journal = {Proceedings of the ACM on Programming Languages},
volume = {7},
number = {PLDI},
year = {2023},
doi = {10.1145/3591222}
}