ACORN: Network Control Plane Abstraction using Route Nondeterminism

Divya Raghunathan, Ryan Beckett, Aarti Gupta, David Walker

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

Abstract

Networks are hard to configure correctly, and mis-configurations occur frequently, leading to outages or security breaches. Formal verification techniques have been applied to guarantee the correctness of network configurations, thereby improving network reliability. This work addresses verification of distributed network control planes, with two distinct contributions to improve the scalability of verification. Our first contribution is a hierarchy of abstractions of varying precision which introduce nondeterminism into the procedure that routers use to select the best available route. We prove the soundness of these abstractions and show their benefits. Our second contribution is a novel SMT encoding which uses symbolic graphs to encode all possible stable routing trees that are compliant with the given network control plane configurations. We have implemented our abstractions and SMT encoding in a prototype tool called ACORN. Our evaluations show that our abstractions can provide significant relative speedups (up to 323x) in performance, and ACORN can scale up to ≈37, 000 routers in data center benchmarks (with FatTree topologies, running shortest-path routing and valley-free policies) for verifying reachability. This far exceeds the performance of existing control plane verifiers.

Original languageEnglish (US)
Title of host publicationProceedings of the 22nd Conference on Formal Methods in Computer-Aided Design, FMCAD 2022
EditorsAlberto Griggio, Neha Rungta
PublisherInstitute of Electrical and Electronics Engineers Inc.
Pages261-272
Number of pages12
ISBN (Electronic)9783854480532
DOIs
StatePublished - 2022
Event22nd International Conference on Formal Methods in Computer-Aided Design, FMCAD 2022 - Trento, Italy
Duration: Oct 17 2022Oct 21 2022

Publication series

NameProceedings of the 22nd Conference on Formal Methods in Computer-Aided Design, FMCAD 2022

Conference

Conference22nd International Conference on Formal Methods in Computer-Aided Design, FMCAD 2022
Country/TerritoryItaly
CityTrento
Period10/17/2210/21/22

All Science Journal Classification (ASJC) codes

  • Artificial Intelligence
  • Computer Graphics and Computer-Aided Design
  • Safety, Risk, Reliability and Quality
  • Modeling and Simulation

Fingerprint

Dive into the research topics of 'ACORN: Network Control Plane Abstraction using Route Nondeterminism'. Together they form a unique fingerprint.

Cite this