Modular Control Plane Verification via Temporal Invariants

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

Research output: Contribution to journalArticlepeer-review

1 Scopus citations

Abstract

Monolithic control plane verification cannot scale to hyperscale network architectures with tens of thousands of nodes, heterogeneous network policies and thousands of network changes a day. Instead, modular verification offers improved scalability, reasoning over diverse behaviors, and robustness following policy updates. We introduce Timepiece, a new modular control plane verification system. While one class of verifiers, starting with Minesweeper, were based on analysis of stable paths, we show that such models, when deployed naïvely for modular verification, are unsound. To rectify the situation, we adopt a routing model based around a logical notion of time and develop a sound, expressive, and scalable verification engine. Our system requires that a user specifies interfaces between module components. We develop methods for defining these interfaces using predicates inspired by temporal logic, and show how to use those interfaces to verify a range of network-wide properties such as reachability or access control. Verifying a prefix-filtering policy using a non-modular verification engine times out on an 80-node fattree network after 2 hours. However, Timepiece verifies a 2,000-node fattree in 2.37 minutes on a 96-core virtual machine. Modular verification of individual routers is embarrassingly parallel and completes in seconds, which allows verification to scale beyond non-modular engines, while still allowing the full power of SMT-based symbolic reasoning.

Original languageEnglish (US)
Pages (from-to)50-75
Number of pages26
JournalProceedings of the ACM on Programming Languages
Volume7
DOIs
StatePublished - Jun 6 2023

All Science Journal Classification (ASJC) codes

  • Software
  • Safety, Risk, Reliability and Quality

Keywords

  • compositional reasoning
  • formal network verification
  • modular verification

Fingerprint

Dive into the research topics of 'Modular Control Plane Verification via Temporal Invariants'. Together they form a unique fingerprint.

Cite this