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:
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.
Publication Date: Aug-2017
Citation: Beckett, 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.
DOI: 10.1145/3098822.3098834
Pages: 155 - 168
Type of Material: Conference Article
Series/Report no.: SIGCOMM '17;
Journal/Proceeding Title: Proceedings of the Conference of the ACM Special Interest Group on Data Communication
Version: Author's manuscript

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