Kirigami, the Verifiable Art of Network Cutting
Kirigami, the Verifiable Art of Network Cutting
复制标题
DOI：
10.1109/icnp55882.2022.9940333
复制
发表时间：
2022-02
期刊：
影响因子：
--
通讯作者：
Tim Alberdingk Thijm;Ryan Beckett;Aarti Gupta;D. Walker
中科院分区：
文献类型：
--
作者：
Tim Alberdingk Thijm;Ryan Beckett;Aarti Gupta;D. Walker
令人满意的模量理论（SMT）的分析允许对复杂的分布式控制平面路由行为进行详尽的推理，从而在任意条件下验证路由。为了提高SMT求解的可扩展性，我们引入了一种模块化验证方法来进行网络控制平面验证，在此中，我们将网络切成较小的片段。用户指定了一个注释的剪辑，该切割描述了如何从整体网络中生成这些片段，我们使用这些注释来独立验证每个片段，以定义假设并保证类似于假设寄存者推理的片段。我们证明，相对于整体网络的验证，这种模块化网络验证过程是合理的。我们将此程序实施为Kirigami，是NV [25]的扩展[25] - 网络验证语言和工具 - 并在具有综合政策的工业拓扑上进行评估。我们观察到端到端NV验证时间的10倍改善，SMT求解时间最多提高了6个数量级。
Satisfiability Modulo Theories (SMT)-based analysis allows exhaustive reasoning over complex distributed control plane routing behaviors, enabling verification of routing under arbitrary conditions. To improve scalability of SMT solving, we introduce a modular verification approach to network control plane verification, where we cut a network into smaller fragments. Users specify an annotated cut which describes how to generate these fragments from the monolithic network, and we verify each fragment independently, using these 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 [25] - a network verification language and tool - and evaluate it on industrial topologies with synthesized policies. We observe a 10x improvement in end-to-end NV verification time, with SMT solve time improving by up to 6 orders of magnitude.