A general approach to network configuration verification

Ryan Beckett, Aarti Gupta, Ratul Mahajan, David Walker

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

37 Scopus citations

Abstract

We present Minesweeper, a tool to verify that a network satisfies a wide range of intended properties such as reachability or isolation among nodes, waypointing, black holes, bounded path length, load-balancing, functional equivalence of two routers, and fault-tolerance. Minesweeper translates network configuration files into a logical formula that captures the stable states to which the network forwarding will converge as a result of interactions between routing protocols such as OSPF, BGP and static routes. It then combines the formula with constraints that describe the intended property. If the combined formula is satisfiable, there exists a stable state of the network in which the property does not hold. Otherwise, no stable state (if any) violates the property. We used Minesweeper to check four properties of 152 real networks from a large cloud provider. We found 120 violations, some of which are potentially serious security vulnerabilities. We also evaluated Minesweeper on synthetic benchmarks, and found that it can verify rich properties for networks with hundreds of routers in under five minutes. This performance is due to a suite of model-slicing and hoisting optimizations that we developed, which reduce runtime by over 460x for large networks.

Original languageEnglish (US)
Title of host publicationSIGCOMM 2017 - Proceedings of the 2017 Conference of the ACM Special Interest Group on Data Communication
PublisherAssociation for Computing Machinery, Inc
Pages155-168
Number of pages14
ISBN (Electronic)9781450346535
DOIs
StatePublished - Aug 7 2017
Event2017 Conference of the ACM Special Interest Group on Data Communication, SIGCOMM 2017 - Los Angeles, United States
Duration: Aug 21 2017Aug 25 2017

Publication series

NameSIGCOMM 2017 - Proceedings of the 2017 Conference of the ACM Special Interest Group on Data Communication

Other

Other2017 Conference of the ACM Special Interest Group on Data Communication, SIGCOMM 2017
CountryUnited States
CityLos Angeles
Period8/21/178/25/17

    Fingerprint

All Science Journal Classification (ASJC) codes

  • Computer Networks and Communications
  • Signal Processing
  • Electrical and Electronic Engineering
  • Communication

Keywords

  • Control plane analysis
  • Network verification

Cite this

Beckett, R., Gupta, A., Mahajan, R., & Walker, D. (2017). A general approach to network configuration verification. In SIGCOMM 2017 - Proceedings of the 2017 Conference of the ACM Special Interest Group on Data Communication (pp. 155-168). (SIGCOMM 2017 - Proceedings of the 2017 Conference of the ACM Special Interest Group on Data Communication). Association for Computing Machinery, Inc. https://doi.org/10.1145/3098822.3098834