Skip to main content

A general approach to network configuration verification

Author(s): Beckett, Ryan; Gupta, Aarti; Mahajan, Ratul; Walker, David

To refer to this page use:
Full metadata record
DC FieldValueLanguage
dc.contributor.authorBeckett, Ryan-
dc.contributor.authorGupta, Aarti-
dc.contributor.authorMahajan, Ratul-
dc.contributor.authorWalker, David-
dc.identifier.citationBeckett, Ryan, Gupta, Aarti, Mahajan, Ratul and Walker, David. A General Approach to Network Configuration Verification. Proceedings of the Conference of the ACM Special Interest Group on Data Communication (2017): 155–168.
dc.description.abstractWe 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.en_US
dc.format.extent155 - 168en_US
dc.relation.ispartofProceedings of the Conference of the ACM Special Interest Group on Data Communicationen_US
dc.relation.ispartofseriesSIGCOMM '17;-
dc.rightsAuthor's manuscripten_US
dc.titleA general approach to network configuration verificationen_US
dc.typeConference Articleen_US

Files in This Item:
File Description SizeFormat 
GeneralApproachNetworkConfigVerification.pdf728.17 kBAdobe PDFView/Download

Items in OAR@Princeton are protected by copyright, with all rights reserved, unless otherwise indicated.