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.

翻译：我们在网络控制平面核查中采用了模块化核查方法,我们把网络切成小块,以提高SMT的可扩缩性。用户提供了附加说明的剪切,描述了如何从单板网络中产生这些碎片,我们独立地核查每个碎片,我们使用说明来界定对类似假设-保障推理的碎片的假设和保障。我们证明这个模块化网络核查程序对于对单一网络的核查是合理和完整的。我们用Kirigami(NV的延伸-网络核查语言和工具)来实施这个程序,并用综合政策来评估工业形态。我们观察到在终端-终端的NV核查时间里有2-8x的改进,SMT将时间改进到6个数量级。