Abstract: The increasing complexity of modern computer networks has far outpaced the development of tools to manage their operation. We are developing systems which simplify network security and management by formally reasoning about network-wide forwarding behavior. Our first data plane verification system, Anteater [SIGCOMM'11], revealed multiple real-world bugs in a large university network, including forwarding loops and stale ACL rules. VeriFlow [HotSDN'12 and NSDI'13] checks network-wide invariants in real time as each forwarding rule is inserted, optionally blocking vulnerabilities from being introduced into the network. Our current OpenFlow-based implementation can perform rigorous checking within hundreds of microseconds per rule insertion. This talk presents work with Ahmed Khurshid, Haohui Mai, Kelvin Zou, Wenxuan Zhou, Rachit Agarwal, Matthew Caesar, and Sam King.

Speaker bio: P. Brighten Godfrey is an assistant professor in the Department of Computer Science at the University of Illinois at Urbana-Champaign. He completed his Ph.D. at UC Berkeley in May 2009, advised by Ion Stoica, and his B.S. at Carnegie Mellon University in 2002. His research interests lie in the design and analysis of networked systems. He is a winner of the 2012 National Science Foundation CAREER Award, the 2012 IEEE Communications Society & Information Theory Society Joint Paper Award, the 2010 IEEE Communications Society Data Storage Technical Committee Best Paper Award, and a best paper award at HotSDN 2012.