论文标题
基里加米（Kirigami），网络切割的可验证艺术
Kirigami, the Verifiable Art of Network Cutting
论文作者
论文摘要
我们引入了一种模块化验证方法来进行网络控制平面验证，在此我们将网络切成较小的片段以提高SMT求解的可扩展性。用户提供了一个带注释的剪辑，该剪辑描述了如何从整体网络中生成这些片段，我们使用注释来独立验证每个片段，以定义假设并保证类似于假设寄养推理的片段。我们证明，相对于整体网络的验证，这种模块化网络验证过程是合理的。我们将此程序实施为Kirigami，它是NV的扩展 - 网络验证语言和工具 - 并在具有合成的策略的工业拓扑上进行评估。我们观察到端到端NV验证时间的2-8倍改善，SMT求解时间最多提高了6个数量级。
We introduce a modular verification approach to network control plane verification, where we cut a network into smaller fragments to improve the scalability of SMT solving. Users provide an annotated cut which describes how to generate these fragments from the monolithic network, and we verify each fragment independently, using the annotations to define assumptions and guarantees over fragments akin to assume-guarantee reasoning. We prove this modular network verification procedure is sound and complete with respect to verification over the monolithic network. We implement this procedure as Kirigami, an extension of NV - a network verification language and tool - and evaluate it on industrial topologies with synthesized policies. We observe a 2-8x improvement in end-to-end NV verification time, with SMT solve time improving by up to 6 orders of magnitude.
