Diagnosing security and correctness problems in networks is time-consuming and error-prone. Existing tools to assist operators are ad hoc, or focus on analyzing control plane configuration, which can miss bugs and is hard to generalize across protocols.
We are developing an alternative approach: diagnosing problems through static analysis of the data plane. This approach can catch bugs that are invisible at the level of configuration files, and simplifies unified analysis of a network across many protocols and implementations. For example, our tools allow an operator to verify properties such as ensuring that data from one protected VLAN cannot leak onto another; or that no packet can possibly reach a certain server without going through a firewall; or that there exists no forwarding loop.
I will discuss two tools that can diagnose problems through static analysis of the data plane. Anteater checks invariants in the data plane in an offline manner. Applied to a large university network, Anteater revealed 23 bugs, including forwarding loops and stale ACL rules, with only five false positives. VeriFlow is a tool that checks network-wide invariants in real time, as the network state evolves. VeriFlow interoperates with an OpenFlow controller to check network-wide invariants in real time as each forwarding rule is inserted, optionally blocking any rules that violate an invariant. Our current implementation can perform rigorous checking within hundreds of microseconds per rule insertion.
This is work with Ahmed Khurshid, Kelvin Zou, Wenxuan Zhou, Haohui Mai, Rachit Agarwal, Matthew Caesar, and Sam King.
Brighten Godfreyis 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, and the 2010 IEEE Communications Society Data Storage Technical Committee Best Paper Award.