Design Verification: Treating Networks Like Programs or Chips

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 would like to explore fresh approaches and contrast them to standard approaches to verification using model checking, SAT solvers, and so forth. While network verification is similar to finite state machine verification, there is domain-specific structure that can be exploited and a different set of properties to verify. Early results suggest that concepts from EDA and program verification can be leveraged to create what might be termed Network Design Automation. What might the equivalent of Layout Versus Schematic tools or Specification Mining be? Could there be a theory of types for networks? Our panelists will explore this vision, touching upon modular network semantics, language design, performance invariants, and interactive network debuggers. We will also explore with the help of SDN experts the connections between this vision and the vision of Software Designed Networks.

Speaker Details

Nikolaj Bjorner is a Principal Researcher at Microsoft Research, Redmond, working in the area of Automated Theorem Proving and Software Engineering. His current main line of work is around the state-of-the art theorem prover Z3, which is used as a foundation of several software engineering tools. Previously, he designed the DFSR, Distributed File System – Replication, co-designed RDC, remote differential compression, protocol both shipped with Windows Server since 2005 and before that worked on distributed file sharing systems at a startup XDegrees, and program synthesis and transformation systems at the Kestrel Institute. He received his master’s and Ph.D. degrees in computer science from Stanford University, and spent the first three years of university at DTU and DIKU. Learn more about Nikolaj.

Ratul Mahajan is a Principal Researcher at Microsoft Research and an Affiliate Professor at the University of Washington. His research interests include all aspects of networked systems. His current work focuses on network verification and optical networks, and his past work spans software-defined networking, Internet routing and measurements, incentive-compatible protocol design, vehicular and wireless networks, and connected homes. He has published over 50 papers in top-tier venues such as SIGCOMM, SOSP, MobiCom, and CHI. He is a winner of the ACM SIGCOMM Test of Time award, ACM SIGCOMM Rising Star award, the William R. Bennett prize, the SIGCOMM best paper award, and Microsoft Research Graduate Fellowship.

Nate Foster is an assistant professor of Computer Science at Cornell University. His research focuses on developing language abstractions and tools for building reliable systems. He received a PhD in Computer and Information Science from the University of Pennsylvania in 2009, an MPhil in History and Philosophy of Science and Medicine from Cambridge University in 2008, and a BA in Computer Science from Williams College in 2001. His awards include a Sloan Research Fellowship, an NSF CAREER Award, a Most Influential POPL Paper Award, a Tien ’72 Teaching Award, an NSDI ’13 Community Award, a Yahoo! Academic Career Enhancement Award, and the Penn CIS Morris and Dorothy Rubinoff Award.

Sharad Malik received the B. Tech. degree in Electrical Engineering from the Indian Institute of Technology, New Delhi in 1985 and the M.S. and Ph.D. degrees in Computer Science from the University of California, Berkeley in 1987 and 1990 respectively. Currently he is the George Van Ness Lothrop Professor of Engineering at Princeton University and the chair of the Department of Electrical Engineering. Previously he served as the director of the Keller Center for Innovation in Engineering Education at Princeton University (2006-2011) and the director of the multi-university Gigascale Systems Research Center (2009-2012).

George Varghese obtained his Ph.D. in 1992 from MIT. He worked from 1993-1999 at Washington University, and from 1999 to 2012 at UCSD, both as professor of computer science. He won the ONR Young Investigator Award in 1996, and was elected to be a Fellow of the Association for Computing Machinery (ACM) in 2002. His book, Network Algorithmics, was published in December 2004 by Morgan-Kaufman. In May 2004, he co-founded NetSift Inc., which was acquired by Cisco Systems in 2005. He joined Microsoft Research in 2012. He has received the 2014 ACM SIGCOMM Award, the 2014 IEEE Koji Kobayashi Computers and Communications Award, and the 2015 Distinguished Alumni Award from IIT Bombay.

Geoffrey G. Xie is a professor and associated chair of the computer science department, Naval Postgraduate School. He received the BS degree in computer science from Fudan University, China, and the PhD degree in computer sciences from the University of Texas at Austin. He was a visiting scholar in the School of Computer Science at Carnegie Mellon University from 2003 to 2004, and the Computer Laboratory of the University of Cambridge, United Kingdom, from 2010 to 2011. He has published more than 70 articles in various areas of networking. He co-chaired the ACM SIGCOMM Internet Network Management Workshop in 2007. He won the best paper award at the 2007 IEEE ICNP conference and the 2011 IEEE Fred W. Ellersick Award. His current research interests include formal network analysis, routing design and theories, and abstraction driven design of enterprise networks.

Series:
Microsoft Research Faculty Summit
Date:
Speakers:
Geoffrey G. Xie, George Varghese, Nate Foster, Nikolaj Bjorner, and Ratul Mahajan
Affiliation:
Microsoft Research, Cornell University, Princeton University, Naval Postgraduate School

Series: Microsoft Research Faculty Summit