Network Control Plane Synthesis and Verification

Abstract

Computer networks have become an integral part of modern infrastructure, and as the world continues to become increasingly interconnected and more devices come online, the importance of networks will only continue to grow. A critical component of networks is a process called routing, whereby the network determines how to move data from point A to point B as changes occur dynamically (e.g., when new devices connect or equipment fails). Routing is traditionally achieved through the manual configuration of one or more distributed protocols that exchange messages about available routes to different destinations. Manual configuration lets a network operator tune various low-level protocol parameters to accommodate the different economic-, performance-, and robustness-related objectives that they may have for the network. Unfortunately, the low-level nature of existing configuration primitives and the scale of modern networks makes it difficult for humans to predict the impact of configuration on all possible runtime behaviors of the network, often resulting in configuration bugs.

This dissertation develops two complementary techniques for proactively finding and preventing bugs in configurations. The first technique is verification. Given a collection of router configurations and a high-level specification of what the network should do (e.g., certain devices should be reachable), verification aims to ensure that the configurations implement this high-level specification correctly for all possible network behaviors. To address this problem, we develop a formal model of network routing protocols and show how many common protocols can be translated to logic constraints that existing constraint solvers can solve to find (or prove the absence of) bugs. The second technique is synthesis. Given a high-level specification of what the network should do, synthesis aims to produce a collection of configurations that faithfully implement the specification for all possible dynamic network conditions. We develop a new high-level language for describing end-to-end network behavior and demonstrate an efficient synthesis algorithm that can generate correct configurations. Throughout the development of both techniques, we show the importance of "abstraction'' in speeding up each technique by several orders of magnitude.