A general approach to network configuration verification

Ryan Beckett, Aarti Gupta, Ratul Mahajan, David P. Walker

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

26 Citations (Scopus)

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

Routers
Fault tolerance
Routing protocols
Resource allocation
equivalence
tolerance
social isolation
vulnerability
present
interaction
performance

All Science Journal Classification (ASJC) codes

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

Cite this

Beckett, R., Gupta, A., Mahajan, R., & Walker, D. P. (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
Beckett, Ryan ; Gupta, Aarti ; Mahajan, Ratul ; Walker, David P. / A general approach to network configuration verification. SIGCOMM 2017 - Proceedings of the 2017 Conference of the ACM Special Interest Group on Data Communication. Association for Computing Machinery, Inc, 2017. pp. 155-168 (SIGCOMM 2017 - Proceedings of the 2017 Conference of the ACM Special Interest Group on Data Communication).
@inproceedings{156dd858dd0547b69ca4aa7cffe6541d,
title = "A general approach to network configuration verification",
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.",
author = "Ryan Beckett and Aarti Gupta and Ratul Mahajan and Walker, {David P.}",
year = "2017",
month = "8",
day = "7",
doi = "10.1145/3098822.3098834",
language = "English (US)",
series = "SIGCOMM 2017 - Proceedings of the 2017 Conference of the ACM Special Interest Group on Data Communication",
publisher = "Association for Computing Machinery, Inc",
pages = "155--168",
booktitle = "SIGCOMM 2017 - Proceedings of the 2017 Conference of the ACM Special Interest Group on Data Communication",

}

Beckett, R, Gupta, A, Mahajan, R & Walker, DP 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. SIGCOMM 2017 - Proceedings of the 2017 Conference of the ACM Special Interest Group on Data Communication, Association for Computing Machinery, Inc, pp. 155-168, 2017 Conference of the ACM Special Interest Group on Data Communication, SIGCOMM 2017, Los Angeles, United States, 8/21/17. https://doi.org/10.1145/3098822.3098834

A general approach to network configuration verification. / Beckett, Ryan; Gupta, Aarti; Mahajan, Ratul; Walker, David P.

SIGCOMM 2017 - Proceedings of the 2017 Conference of the ACM Special Interest Group on Data Communication. Association for Computing Machinery, Inc, 2017. p. 155-168 (SIGCOMM 2017 - Proceedings of the 2017 Conference of the ACM Special Interest Group on Data Communication).

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

TY - GEN

T1 - A general approach to network configuration verification

AU - Beckett, Ryan

AU - Gupta, Aarti

AU - Mahajan, Ratul

AU - Walker, David P.

PY - 2017/8/7

Y1 - 2017/8/7

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=85029448893&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=85029448893&partnerID=8YFLogxK

U2 - 10.1145/3098822.3098834

DO - 10.1145/3098822.3098834

M3 - Conference contribution

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

SP - 155

EP - 168

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

PB - Association for Computing Machinery, Inc

ER -

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