Probabilistic Verification of Network Configurations
METADATA ONLY
Author / Producer
Date
2020
Publication Type
Conference Paper
ETH Bibliography
yes
Citations
Altmetric
METADATA ONLY
Data
Rights / License
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.
Permanent link
Publication status
published
External links
Editor
Book title
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
Journal / series
Volume
Pages / Article No.
750 - 764
Publisher
Association for Computing Machinery
Event
ACM SIGCOMM 2020 (virtual)
Edition / version
Methods
Software
Geographic location
Date collected
Date created
Subject
Network Analysis; Failures; Probabilisti inference; Cold edges
Organisational unit
09477 - Vanbever, Laurent / Vanbever, Laurent
03948 - Vechev, Martin / Vechev, Martin
Notes
Due to the Corona virus (COVID-19) the conference was conducted virtually.