Please note: ROOM CHANGE for Ryan Beckett's Pre FPO today. Ryan Beckett will present his Pre-FPO on Tuesday, November 14, 2017 at 11:30am in CS 105 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 Title: Network Control Plane Verification and Synthesis Abstract: 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. _______________________________________________ talks mailing list talks@lists.cs.princeton.edu To edit subscription settings or remove yourself, use this link: https://lists.cs.princeton.edu/mailman/listinfo/talks