George Varghese

UCLA

Talk Title: Network Design Automation- When Clarke Meets Cerf

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. Taking our cue from program and hardware verification, we suggest fresh approaches. I will first describe 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 to scale better than off-the shelf model checkers. Next, I show how to 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 structure. While header space models allow us to verify the forwarding tables in routers, they require a specification which is often unavailable. In the second part of the talk I will show to use network specific data mining to find bugs in router configurations without a specification by leveraging the role structure of routers. I will end with a vision for what we call Network Design Automation to build a suite of tools for networks inspired by the Electronic Design Automation Industry. (With collaborators at Edinburgh, MSR, Stanford, and UCLA.)

Bio

George Varghese is a Chancellor's Professor of Computer Science at UCLA. His research interests center around network algorithmics (building fast routers) and network verification (building tools for static and dynamic verification of operational networks). He 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. From 2012-2016, he was a Principal Researcher and Partner at Microsoft Research. 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). 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 was elected to the National Academy of Engineering in 2017. He won the IEEE Kobayashi Award for Computers and Communications in 2014, and the SIGCOMM Lifetime Achievement Award for networking in 2014. He was elected to the National Academy of Engineering in 2017.