Kirigami, the Verifiable Art of Network Cutting

Timothy Alberdingk Thijm, Ryan Beckett, Aarti Gupta, David Walker

Research output: Chapter in Book/Report/Conference proceedingConference contribution

2 Scopus citations

Abstract

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.

Original languageEnglish (US)
Title of host publication2022 IEEE 30th International Conference on Network Protocols, ICNP 2022
PublisherIEEE Computer Society
ISBN (Electronic)9781665482349
DOIs
StatePublished - 2022
Event30th IEEE International Conference on Network Protocols, ICNP 2022 - Lexington, United States
Duration: Oct 30 2022Nov 2 2022

Publication series

NameProceedings - International Conference on Network Protocols, ICNP
Volume2022-October
ISSN (Print)1092-1648

Conference

Conference30th IEEE International Conference on Network Protocols, ICNP 2022
Country/TerritoryUnited States
CityLexington
Period10/30/2211/2/22

All Science Journal Classification (ASJC) codes

  • Computer Networks and Communications
  • Software

Keywords

  • control plane verification
  • modular verification
  • network control plane
  • routing protocols

Fingerprint

Dive into the research topics of 'Kirigami, the Verifiable Art of Network Cutting'. Together they form a unique fingerprint.

Cite this