Skip navigation
Please use this identifier to cite or link to this item: http://arks.princeton.edu/ark:/88435/dsp01d217qs28v
Title: Network Control Plane Synthesis and Verification
Authors: Beckett, Ryan
Advisors: Walker, David
Contributors: Computer Science Department
Keywords: Computer Networks
Control Plane
Routing
Synthesis
Verification
Subjects: Computer science
Issue Date: 2018
Publisher: Princeton, NJ : Princeton University
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.
URI: http://arks.princeton.edu/ark:/88435/dsp01d217qs28v
Alternate format: The Mudd Manuscript Library retains one bound copy of each dissertation. Search for these copies in the library's main catalog: catalog.princeton.edu
Type of Material: Academic dissertations (Ph.D.)
Language: en
Appears in Collections:Computer Science

Files in This Item:
File Description SizeFormat 
Beckett_princeton_0181D_12696.pdf3.49 MBAdobe PDFView/Download


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