Network Verification - When Hoare Meets Cerf 
 |
Wednesday, September 2, 2015 George Varghese
|
ABSTRACT:
Surveys reveal that network outages are prevalent, and that many outages take hours to resolve, resulting in significant lost revenue. Many bugs are caused by errors in configuration files which are programmed using arcane, low-level languages, akin to machine code. Further, mistakes are often hunted down using rudimentary tools.
Taking our cue from program and hardware verification, we suggest fresh approaches. Our first attempt was a geometric model of network forwarding called Header Space. While header space analysis is similar to finite state machine verification, we exploit domain-specific structure and verify different properties.
I will describe recent results where we exploit physical symmetry to scale network verification for large data centers. While Emerson and Sistla showed how to exploit symmetry for model checking in 1996, they exploited symmetry on the logical Kripke sructure. Similarly, I show how symbolic execution in test generation in systems such as KLEE and DART suggests new approaches to automatic test packet generation and BGP configuration testing.
Speculative questions abound. Could there be a theory of types for networks? What should a modular network semantics look like? This is joint work with collaborators at Berkeley, CMU, Edinburgh, MSR, Stanford, and UCLA.
BIOGRAPHY:
George Varghese received his Ph.D. in 1992 from MIT. From 1993-1999, he was a professor at Washington University, and at UCSD from 1999 to 2013. He was the Distinguished Visitor in the computer science department at Stanford University from 2010-2011. He joined Microsoft Research in 2012.
His book "Network Algorithmics" was published in December 2004 by Morgan-Kaufman. In May 2004, he co-founded NetSift, which was acquired by Cisco Systems in 2005. With colleagues, he has won best paper awards at SIGCOMM (2014), ANCS (2013), OSDI (2008), PODC (1996), and the IETF Applied Networking Prize (2013). He won the Kobayashi Award and the SIGCOMM Lifetime Award, both in 2014, and the IIT Bombay Distinguished Alumni Award in 2015.
| Return to EECS Joint Colloquium |