Networks today achieve robustness not by adhering to precise formal specifications but by building implementations that tolerate modest deviations from correct behavior. This philosophy can be seen in the slogan used by the Internet Engineering Task Force," we believe in rough consensus and running code," and by Jon Postel’s famous dictum to “be conservative in what you do, be liberal in what you accept from others.” But as networks have grown in scale and complexity, the frequency of faults has led to new interest in techniques for formally verifying network behavior.

This talk will discuss recent progress on practical tools for specifying and verifying formal properties of networks. In the first part of the talk, I will present p4v, a tool for verifying the low-level code that executes on individual devices such as routers and firewalls. In the second part of the talk, I will present NetKAT, a formal system for specifying and verifying network-wide behavior. In the third part of the talk, I will highlight some challenges and opportunities for future research in network verification.

Nate Foster is an Associate Professor of Computer Science at Cornell University and a Principal Research Engineer at Barefoot Networks. The goal of his research is to develop languages and tools that make it easy for programmers to build secure and reliable systems. His current work focuses on the design and implementation of languages for programming software-defined networks. In the past he has also worked on bidirectional languages (also known as “lenses”), database query languages, data provenance, type systems, mechanized proof, and formal semantics. He received a PhD in Computer Science from the University of Pennsylvania. His honors include a Sloan Research Fellowship, an NSF CAREER Award, a Most Influential POPL Paper Award, and the SIGCOMM Rising Star Award.