TY - GEN
T1 - NV
T2 - 41st ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2020
AU - Giannarakis, Nick
AU - Loehr, Devon
AU - Beckett, Ryan
AU - Walker, David
N1 - Publisher Copyright:
© 2020 ACM.
PY - 2020/6/11
Y1 - 2020/6/11
N2 - 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.
AB - 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.
KW - Control Plane Analysis
KW - Intermediate Verification Language
KW - Network Simulation
KW - Network Verification
KW - Router Configuration Analysis
UR - http://www.scopus.com/inward/record.url?scp=85086825243&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85086825243&partnerID=8YFLogxK
U2 - 10.1145/3385412.3386019
DO - 10.1145/3385412.3386019
M3 - Conference contribution
AN - SCOPUS:85086825243
T3 - Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI)
SP - 958
EP - 973
BT - PLDI 2020 - Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation
A2 - Donaldson, Alastair F.
A2 - Torlak, Emina
PB - Association for Computing Machinery
Y2 - 15 June 2020 through 20 June 2020
ER -