Network Verification: Lessons Learned and Outlook

LUNCH
Lunch will be served at 11:45 AM

ABSTRACT
Computer networks are at the foundation of modern society. When they fail, banks go offline, airplanes stop flying, emergency numbers stop working, and businesses lose millions of dollars. Over the last decade, the networking community has made significant progress toward technology that can provide formal correctness guarantees for network behavior. I co-developed one such tool, called Batfish, that is in use at many large enterprises. I'll share key lessons from its evolution from a research prototype to an industrial-strength product, such as how Datalog-based logic programming had significant limitations and how binary decision diagrams (BDDs) proved highly versatile. I will also outline key challenges in using current verification technology and what is needed to further improve network reliability by an order of magnitude.

SPEAKER BIO
Ratul Mahajan is a faculty member at the University of Washington (Paul G. Allen School of Computer Science). He is also the co-director of UW FOCI (Future of Cloud Infrastructure) and an Amazon Scholar. Ratul is a computer systems researcher with a networking focus and has worked on a broad set of topics, including network verification, connected homes, network programming, optical networks, Internet routing and measurements, and mobile systems. Many of the technologies that he has helped develop are part of real-world systems at Microsoft and other companies. Ratul has been recognized as an ACM Distinguished Scientist, an ACM SIGCOMM Rising Star, and a Microsoft Research Graduate Fellow. His papers have won the ACM SIGCOMM Test-of-Time Award, the IEEE William R. Bennett Prize, the ACM SIGCOMM Best Paper Awards (twice), and the HVC Best Paper Award.