Kirigami：可验证的网络切割艺术
网络与互联网体系结构
2023-04-10 v1 形式语言与自动机理论
摘要
我们引入一种模块化的验证方法用于网络控制平面验证，将网络切割为更小的片段以提升 SMT 求解的可扩展性。用户提供带标注的切割，描述如何从单体网络生成这些片段，我们独立验证每个片段，利用标注定义片段间的假设与保证，类似于假设-保证推理。我们证明该模块化网络验证过程相对于单体网络验证是可靠且完备的。我们将该过程实现为 Kirigami——网络验证语言与工具 NV 的扩展——并在带有合成策略的工业拓扑上评估。我们观察到端到端 NV 验证时间提升 2-8 倍，SMT 求解时间最高提升 6 个数量级。
引用
@article{arxiv.2202.06098,
title = {Kirigami, the Verifiable Art of Network Cutting},
author = {Tim Alberdingk Thijm and Ryan Beckett and Aarti Gupta and David Walker},
journal= {arXiv preprint arXiv:2202.06098},
year = {2023}
}
备注
30 pages, 9 figures, submitted to CAV 2022