DATE: Friday, February 13, 2015
TIME: 10:30 am - 12:00 pm
PLACE: GHC 6115
SPEAKER: George Varghese, Microsoft Research
TITLE: From EDA to NDA -- Treating Networks like Chips and Programs
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 such as Ping and Traceroute.
Taking our cue from other fields such as hardware design, we suggest fresh approaches. Our first attempt was a geometric model of network forwarding called Header Space together with parsers that convert router configurations to header space representations. While header space analysis is similar to finite state machine verification, there is domain-specific structure that can be exploited and a different set of properties to verify. I will describe a series of tools including Hassel (a "static checker" that identifies loops and isolation failures) and ATPG (a "dynamic checker" which identifies "run-time" faults and performance problems by automatically generating test packets). I will describe experience applying these tools to the Google WAN, the Stanford backbone, and Microsoft data centers, and the domain restrictions that led us to use different techniques from earlier methods used in the verification community.
These results suggest that concepts from EDA and program verification can be leveraged to create what might be termed "Network Design Automation". For example, what might be the equivalent of Layout Versus Schematic tools or Specification Mining? Could there be a theory of types for networks? The second part of this talk will explore this vision, touching upon modular network semantics, language design, performance invariants, and interactive network debuggers. This is joint work with collaborators at Berkeley, Cisco, MSR, and Stanford.
BIO:
George Varghese is a Principal Researcher and Partner at Microsoft Research since Aug 2012. His current research interests center around network verification --- asking if networks can be treated like computer programs or hardware circuits in order to obtain tools for static and dynamic verification, debugging and synthesis, and using these tools to proactively find bugs in operational networks including Microsoft's Azure.
He received his Ph.D. in 1992 from MIT after working at DEC designing DECNET protocols and products, including the bridge architecture and Gigaswitch. 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.
Together with colleagues, he has 22 patents awarded in the general field of Network Algorithmics. Several of the algorithms he helped develop appear in commercial systems including Linux (timing wheels), the Cisco GSR (DRR), and Microsoft Windows (IP lookups). He helped design the hardware lookup engine for Procket's 40 Gbps router. He has been on the advisory boards of Memoir, Jibe, Sanera, and SwitchOn, and consulted for ST MicroElectronics, AOL, and Fujitsu. In May 2004, he co-founded NetSift Inc., where he was President and CTO. NetSift was acquired by Cisco Systems in 2005. His book "Network Algorithmics" on fast router and endnode implementations was published in 2004 by Morgan-Kaufman.
He has written over 100 papers, mostly on networking, but also on computer architecture, genomics, and databases. After Dijkstra's early work, he helped develop general techniques for self-stabilization, an abstraction of a strong network fault-tolerance property. His Erdos number is 2 via mathematicians Ron and Fan Graham. He won the IEEE Kobayashi Award for Computers and Communications in 2014, and the SIGCOMM Lifetime Award in 2014. He has been a Fellow of the ACM since 2002 and an ONR Young Investigator. He was PC co-chair of SIGCOMM 2012 and general co-chair of SIGCOMM 2001.
He won the UCSD Best Teacher Award (2001) and the Graduate Mentor of the Year Award at Washington University (1997). With colleagues, he has won best paper awards at SIGCOMM (2014), ANCS (2013), OSDI (2008) and PODC (1996), and the IETF Applied Networking Prize (2013).
VISITOR HOST: Srinivasan Seshan
VISITOR COORDINATOR: Angela Miller, amiller@cs.cmu.edu, 8-6645
SDI / ISTC SEMINAR QUESTIONS?
Karen Lindenfelser, 86716, or visit www.pdl.cmu.edu/SDI/