NV: An intermediate language for verification of network control planes

Nick Giannarakis, Devon Loehr, Ryan Beckett, David Walker

Research output: Chapter in Book/Report/Conference proceedingConference contribution

1 Scopus citations

Abstract

Network misconfiguration has caused a raft of high-profile outages over the past decade, spurring researchers to develop a variety of network analysis and verification tools. Unfortunately, developing and maintaining such tools is an enormous challenge due to the complexity of network configuration languages. Inspired by work on intermediate languages for verification such as Boogie and Why3, we develop NV, an intermediate language for verification of network control planes. NV carefully walks the line between expressiveness and tractability, making it possible to build models for a practical subset of real protocols and their configurations, and also facilitate rapid development of tools that outperform state-of-the-art simulators (seconds vs minutes) and verifiers (often 10x faster). Furthermore, we show that it is possible to develop novel analyses just by writing new NV programs. In particular, we implement a new fault-tolerance analysis that scales to far larger networks than existing tools.

Original languageEnglish (US)
Title of host publicationPLDI 2020 - Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation
EditorsAlastair F. Donaldson, Emina Torlak
PublisherAssociation for Computing Machinery
Pages958-973
Number of pages16
ISBN (Electronic)9781450376136
DOIs
StatePublished - Jun 11 2020
Event41st ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2020 - London, United Kingdom
Duration: Jun 15 2020Jun 20 2020

Publication series

NameProceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI)

Conference

Conference41st ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2020
CountryUnited Kingdom
CityLondon
Period6/15/206/20/20

All Science Journal Classification (ASJC) codes

  • Software

Keywords

  • Control Plane Analysis
  • Intermediate Verification Language
  • Network Simulation
  • Network Verification
  • Router Configuration Analysis

Fingerprint Dive into the research topics of 'NV: An intermediate language for verification of network control planes'. Together they form a unique fingerprint.

Cite this