Computer Science Department
McGregory Hall, 3rd Floor
13 Oak Drive
Hamilton, NY 13346
Charlotte Jablonski, Administrative Assistant
Start: Tuesday, February 06, 2018, 11:30 a.m.
End: Tuesday, February 06, 2018, 12:20 p.m.
Location: 319 McGregory Hall
Speaker: Nate Foster, Cornell University
Abstract: P4 is a new language for programming network data planes. The language provides domain-specific constructs for describing the input-output formats and functionality of packet-processing pipelines. Unfortunately P4 programs can go wrong in a variety of interesting and frustrating ways including reading uninitialized data, generating malformed packets, and failing to handle exceptions. In this talk, I will present the design and implementation of p4v, a tool for verifying P4 programs. The tool is based on classic software verification techniques (due to Hoare, Dijkstra, Flanagan, Leino, etc.), but adds several important innovations: a novel mechanism for incorporating control-plane assumptions and domain-specific optimizations, both of which are needed to scale up to large programs. I will discuss our experiences applying p4v to a variety of real-world programs including switch.p4, a large program that implements the functionality of a conventional switch.
p4v is joint work with colleagues from Barefoot, Lugano, and Yale.
Bio: 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. He currently serves as chair of the P4 Language Consortium steering committee and as a member of the ACM SIGCOMM Symposium on SDN Research (SOSR) steering committee. 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 an NSF CAREER award and a Sloan Fellowship.