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

[Nicki Gotsis]

Please see revised committee. 





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), Jennifer Rexford, and Nick Feamster ; 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. 

_______________________________________________ 
talks mailing list 
talks at lists.cs.princeton.edu 
To edit subscription settings or remove yourself, use this link: 
https://lists.cs.princeton.edu/mailman/listinfo/talks 
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.cs.princeton.edu/pipermail/talks/attachments/20180715/d142de2c/attachment.html>