[talks] Ryan Beckett will present his Pre-FPO on Tuesday, November 14, 2017 at 11:30am in CS 233
ngotsis at CS.Princeton.EDU
Tue Nov 7 12:36:24 EST 2017
Ryan Beckett will present his Pre-FPO on Tuesday, November 14, 2017 at 11:30am in CS 233.
The members of his committee are as follows:
Advisor: David Walker
Readers: Aarti Gupta, Ratul Mahajan (Microsoft)
Non-Readers: Jennifer Rexford, Nick Feamster
Everyone is invited to attend his talk. The talk title and abstract follow below
Network Control Plane Verification and Synthesis
Network control planes for traditional networks are highly complex distributed systems. Network devices use multiple protocols to exchange routing information about available paths to a destination, and how they process this information depends on their local configuration files. Each configuration file often consists of thousands of lines of assembly-like directives -- making it hard for humans to reason about individual device behaviors and even harder to reason about the network behavior that emerges through the distributed interactions of all devices. Consequently, network misconfiguration caused by human error remains a leading cause of network downtime. In my thesis, I develop novel approaches to automatically verify and synthesize network device configurations in a scalable manner from high-level specifications about their correctness.
In the first part of this talk, I will describe a general approach to network control plane verification based on translating unmodified network configurations into logical formulae that capture both the stable states to which the network protocols converge as well as their impact on packet forwarding. Using an off-the-shelf Satisfiability Modulo Thoery (SMT) solver, we can verify adherence to a wide range of properties including reachability, fault-tolerance, router equivalence, and load balancing, for all possible outcomes of the control plane. In the second part of my talk, I will describe a new high-level network routing language and associated compilation techniques to generate device configurations that are correct-by-construction. Throughout both parts of the talk, I will describe the role of network abstraction in making these approaches scale to large, modern networks.
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the talks