Kirigami, the Verifiable Art of Network Cutting

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

Research output: Contribution to journalArticlepeer-review

Abstract

Satisfiability Modulo Theories (SMT)-based analysis allows exhaustive reasoning over complex distributed control plane routing behaviors, enabling verification of converged routing states 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 that any converged states of the fragments are converged states of the monolithic network, and there exists an annotated cut that can generate fragments corresponding to any converged state of the monolithic network. We implement this procedure as Kirigami, an extension of the network verification language and tool NV, 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)
Pages (from-to)2447-2462
Number of pages16
JournalIEEE/ACM Transactions on Networking
Volume32
Issue number3
DOIs
StatePublished - Jun 1 2024

All Science Journal Classification (ASJC) codes

  • Software
  • Computer Science Applications
  • Computer Networks and Communications
  • Electrical and Electronic Engineering

Keywords

  • Modular verification
  • control plane 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