Skip navigation
Please use this identifier to cite or link to this item:
Title: An Intermediate Language for Network Verification
Authors: Giannarakis, Nick
Advisors: Walker, David P
Contributors: Computer Science Department
Keywords: Computer networks
Network Analysis
Network Fault-Tolerance
Network Reliability
Subjects: Computer science
Issue Date: 2020
Publisher: Princeton, NJ : Princeton University
Abstract: Computer networks have become an integral part of our daily lives, and essential infrastructure to most industries. This had led to unprecedented growth in their size and complexity. In recent years, misconfiguration-induced outages in networks have become rampant both in frequency and impact. Such misconfigurations are often found in the network's control plane, a distributed system responsible for exchanging routing information between routers. To set the routing policy, operators have to issue per-device configurations in low-level languages, while accounting for interactions with external networks, and potential device or link failures. This is a challenging task, especially for large networks which consist of millions of lines of configuration spread across thousands of devices. To aid operators, researchers have developed a range of static analyses to establish correctness properties of networks. However, developing and maintaining such tools is an enormous undertaking due to the complexity of configuration languages and the plethora of features networking protocols pack. Inspired by intermediate verification languages, such as Boogie and Why3, this dissertation describes the design and implementation of NV, an intermediate language for verification of networks and their configurations. NV was designed to strike a balance between expressiveness, tractability and ease of use. We show that NV is sufficiently expressive via a translation from a practical subset of real protocols (and their configurations) to NV. Furthermore, we explain how NV enabled efficient implementations (often outperforming the state-of-the-art by an order of magnitude) of standard analyses such as network simulation and SMT-based verification. NV also facilitates the rapid development of new analyses; we present the key insights behind a new, highly scalable fault tolerance analysis, as well as its effortless implementation as a "meta-protocol" in NV. Finally, in a similar but orthogonal approach, we present a new take on network compression ---implemented on top of NV--- that significantly speeds up verification of fault-tolerance properties.
Alternate format: The Mudd Manuscript Library retains one bound copy of each dissertation. Search for these copies in the library's main catalog:
Type of Material: Academic dissertations (Ph.D.)
Language: en
Appears in Collections:Computer Science

Files in This Item:
File Description SizeFormat 
Giannarakis_princeton_0181D_13510.pdf739.85 kBAdobe PDFView/Download

Items in Dataspace are protected by copyright, with all rights reserved, unless otherwise indicated.