Computer networks provide the essential communication fabric that underpins almost all modern computing systems. Yet today, most networks are built and operated in an ad hoc manner and require frequent interventions from human experts to remain functional. This talk will make the case for bringing ideas from the formal methods community to bear on practical problems in networking. Starting with the network forwarding plane, we will show how to model network behavior in a way that is amenable to mostly-automated formal reasoning. We will then show how these lower-level models can be used to guide efforts to verify higher layers of the stack, such as the network control planes and even application-level functions.

Nate Foster is an Associate Professor of Computer Science at Cornell University. 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, an MPhil in History and Philosophy of Science from Cambridge University, and a BA in Computer Science from Williams College. His awards include a Sloan Research Fellowship, an NSF CAREER Award, a Most Influential POPL Paper Award, a Tien ’72 Teaching Award, a Google Research Award, a Yahoo! Academic Career Enhancement Award, a Cornell Engineering Research Excellence Award, and the Morris and Dorothy Rubinoff Award.