Probabilistic Verification of Network Configurations
Abstract
Not all important network properties need to be enforced all the time. Often, what matters instead is the fraction of time / probability these properties hold. Computing the probability of a property in a network relying on complex inter-dependent routing protocols is challenging and requires determining all failure scenarios for which the property is violated. Doing so at scale and accurately goes beyond the capabilities of current network analyzers. In this paper, we introduce NetDice, the first scalable and accurate probabilistic network configuration analyzer supporting BGP, OSPF, ECMP, and static routes. Our key contribution is an inference algorithm to efficiently explore the space of failure scenarios. More specifically, given a network configuration and a property φ, our algorithm automatically identifies a set of links whose failure is provably guaranteed not to change whether φ holds. By pruning these failure scenarios, NetDice manages to accurately approximate P(φ). NetDice supports practical properties and expressive failure models including correlated link failures. We implement NetDice and evaluate it on realistic configurations. NetDice is practical: it can precisely verify probabilistic properties in few minutes, even in large networks.
Research Area: Verification and Synthesis
People
BibTex
@INPROCEEDINGS{steffen2020probabilistic,
isbn = {978-1-4503-7955-7},
doi = {10.1145/3387514.3405900},
year = {2020},
booktitle = {SIGCOMM '20: Proceedings of the Annual Conference of the ACM Special Interest Group on Data Communication on the Applications, Technologies, Architectures, and Protocols for Computer Communication},
type = {Conference Paper},
author = {Steffen, Samuel and Gehr, Timon and Tsankov, Petar and Vanbever, Laurent and Vechev, Martin},
abstract = {Not all important network properties need to be enforced all the time. Often, what matters instead is the fraction of time / probability these properties hold. Computing the probability of a property in a network relying on complex inter-dependent routing protocols is challenging and requires determining all failure scenarios for which the property is violated. Doing so at scale and accurately goes beyond the capabilities of current network analyzers.In this paper, we introduce NetDice, the first scalable and accurate probabilistic network configuration analyzer supporting BGP, OSPF, ECMP, and static routes. Our key contribution is an inference algorithm to efficiently explore the space of failure scenarios. More specifically, given a network configuration and a property φ, our algorithm automatically identifies a set of links whose failure is provably guaranteed not to change whether φ holds. By pruning these failure scenarios, NetDice manages to accurately approximate P(φ). NetDice supports practical properties and expressive failure models including correlated link failures.We implement NetDice and evaluate it on realistic configurations. NetDice is practical: it can precisely verify probabilistic properties in few minutes, even in large networks.},
keywords = {Network Analysis; Failures; Probabilisti inference; Cold edges},
language = {en},
address = {New York, NY},
publisher = {Association for Computing Machinery},
title = {Probabilistic Verification of Network Configurations},
PAGES = {750 - 764},
Note = {ACM SIGCOMM 2020 (virtual); Conference Location: New York, NY, USA; Conference Date: August 10-14, 2020; Due to the Corona virus (COVID-19) the conference was conducted virtually.}
}Research Collection: 20.500.11850/432699