Details

Autor(en) / Beteiligte

• Steffen, Samuel
• Gehr, Timon
• Tsankov, Petar
• Vanbever, Laurent
• Vechev, Martin

Titel

Probabilistic Verification of Network Configurations

Ist Teil von

• Proceedings of the Annual conference of the ACM Special Interest Group on Data Communication on the applications, technologies, architectures, and protocols for computer communication, 2020, p.750-764

Ort / Verlag

New York, NY, USA: ACM

Erscheinungsjahr

2020

Quelle

ACM Digital Library (Association for Computing Machinery)

Beschreibungen/Notizen

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