Computing + Mathematical Sciences Lecture

Network outages are prevalent and result in significant lost revenue.  Network bugs are still hunted down using crude tools such as Ping. Given that existing networks are hard enough to verify, Software Designed Networks (SDNs) - which allow customized networks – will be a greater challenge.

Since the early 70's Caltech has been a leader in VLSI design methodologies.  Inspired by hardware design, we suggest fresh approaches to network verification and design.   I will describe Header Space, a geometric model of network forwarding which abstracts across the messy details of Internet devices.  While header space analysis is similar to model checking, there is domain-specific structure that can be exploited and different properties to verify.  I will describe tools including Hassel (a "static checker" that identifies loops and isolation failures) and ATPG (a "dynamic checker" which identifies "run-time" faults).  I will describe experience applying these tools to the Google WAN, the Stanford backbone, and Microsoft data centers.  

The second part of the talk extends this vision to tools for network design inspired by Electronic Design Automation.  We survey new problems suggested by this vision including probabilistic knapsack packing, synthesizing router rules from language specifications, synthesizing rate controllers to maximize revenue, symmetry reductions, and interactive debugging.  This is joint work with collaborators at Berkeley, Cisco, MSR, and Stanford.