An Intermediate Language for Network Verification

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.