基于时态不变式的模块化控制平面验证

单体控制平面验证无法扩展到具有数万节点、异构网络策略和每日数千次网络变更的超大规模网络架构。相反，模块化验证提供了更好的可扩展性、对多样行为的推理能力，以及策略更新后的鲁棒性。我们引入了 Timepiece，一个新的模块化控制平面验证系统。虽然一类验证器（以 Minesweeper 为开端）基于稳定路径分析，但我们表明，此类模型在朴素地用于模块化验证时是不健全的。为纠正该问题，我们采用了一种围绕逻辑时间概念构建的路由模型，并开发了一个健全、富有表达力且可扩展的验证引擎。我们的系统要求用户指定模块组件之间的接口。我们开发了使用受时态逻辑启发的谓词来定义这些接口的方法，并展示了如何利用这些接口验证一系列网络范围属性，如可达性或访问控制。使用非模块化验证引擎验证前缀过滤策略时，在 80 节点胖树网络上 2 小时后超时。然而，Timepiece 在 96 核虚拟机上以 2.37 分钟验证了 2000 节点胖树。对单个路由器的模块化验证极易并行化并在数秒内完成，这使得验证能够扩展到非模块化引擎之外，同时仍允许 SMT 基于符号推理的全部能力。