UCL Discovery
UCL home » Library Services » Electronic resources » UCL Discovery

ProbNV: probabilistic verification of network control planes

Giannarakis, N; Silva, A; Walker, D; (2021) ProbNV: probabilistic verification of network control planes. In: Proceedings of the ACM on Programming Languages (PACMPL). (pp. 90.1-90.30). Association for Computing Machinery (ACM): New York, NY, United States. Green open access

[thumbnail of 3473595.pdf]
3473595.pdf - Published version

Download (383kB) | Preview


ProbNV is a new framework for probabilistic network control plane verification that strikes a balance between generality and scalability. ProbNV is general enough to encode a wide range of features from the most common protocols (eBGP and OSPF) and yet scalable enough to handle challenging properties, such as probabilistic all-failures analysis of medium-sized networks with 100-200 devices. When there are a small, bounded number of failures, networks with up to 500 devices may be verified in seconds. ProbNV operates by translating raw CISCO configurations into a probabilistic and functional programming language designed for network verification. This language comes equipped with a novel type system that characterizes the sort of representation to be used for each data structure: concrete for the usual representation of values; symbolic for a BDD-based representation of sets of values; and multi-value for an MTBDD-based representation of values that depend upon symbolics. Careful use of these varying representations speeds execution of symbolic simulation of network models. The MTBDD-based representations are also used to calculate probabilistic properties of network models once symbolic simulation is complete. We implement the language and evaluate its performance on benchmarks constructed from real network topologies and synthesized routing policies.

Type: Proceedings paper
Title: ProbNV: probabilistic verification of network control planes
Event: ICFP 2021
Open access status: An open access version is available from UCL Discovery
DOI: 10.1145/3473595
Publisher version: https://doi.org/10.1145/3473595
Language: English
Additional information: This work is licensed under a Creative Commons Attribution 4.0 International License.
Keywords: Network Verification, Network Simulation, Probabilistic verification, Probabilistic Network Analysis, Control Plane Analysis, Router Configuration Analysis
UCL classification: UCL
UCL > Provost and Vice Provost Offices > UCL BEAMS
UCL > Provost and Vice Provost Offices > UCL BEAMS > Faculty of Engineering Science
UCL > Provost and Vice Provost Offices > UCL BEAMS > Faculty of Engineering Science > Dept of Computer Science
URI: https://discovery.ucl.ac.uk/id/eprint/10134268
Downloads since deposit
Download activity - last month
Download activity - last 12 months
Downloads by country - last 12 months

Archive Staff Only

View Item View Item