Ryan Beckett will present his FPO, "Network Control Plane Verification and Synthesis" on Monday, 7/23/2018 at 2pm, 101 Marx Hall.

The members of his committee are as follows: Nonreaders: David Walker (adviser), Aarti Gupta, Jennifer Rexford, Nick Feamster, and  Ratul Mahajan (Intentionet); Readers: Aarti Gupta and  Ratul Mahajan (Intentionet) 

All are welcome to attend.  Please see abstract below.

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.