Formal Verification of P4 Programs
Nate Foster, Cornell University
Date: July 19
Abstract:
P4 is a domain-specific language for programming and specifying packet-processing systems. It is based on an elegant design with high-level abstractions like parsers and match-action pipelines that can be compiled to efficient implementations in software or hardware. This tutorial will be structured in two parts; (i) an introduction to the P4 language using hands-on programming examples, and (ii) a discussion of how the Petr4 framework [POPL ’21] can be used to develop language-based verification tools for networks.
Bio: Nate Foster is an Associate Professor of Computer Science at Cornell University, a Principal Research Engineer at Barefoot Networks, and Chair of the P4 Language Technical Steering Team. 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, the SIGCOMM Rising Star Award, a Most Influential POPL Paper Award, a Tien ‘72 Teaching Award, several Google Research Awards, a Yahoo! Academic Career Enhancement Award, a Cornell Engineering Resarch Excellence Award, and the Morris and Dorothy Rubinoff Award.
Introduction to Algebraic Program Analysis
Zak Kincaid (Princeton University) and Tom Reps (University of Wisconsin-Madison)
Date: July 19
Abstract:
Compositional invariant generators operate using a divide-and-conquer strategy: break the program into parts, synthesize invariants for each part, and then combine the results. Compositionality enables invariant generation to scale, to be easily parallelized, to apply to incomplete programs, and to respond quickly to changes to an input program. This tutorial provides an introduction to algebraic program analysis, a framework for compositional invariant generation that builds upon the foundation of abstract algebra and formal language theory. We will show how to design an algebraic program analysis, how to prove that it is correct, and how to implement it. We will show how this framework can be used to solve difficult invariant generation problems (in particular, generation of numerical invariants involving disjunction and non-linear arithmetic), and how it can be applied to recursive programs.
Bios: Zak Kincaid: Zachary Kincaid is an assistant professor in the Department of Computer Science at Princeton University. Kincaid’s research focuses on program analysis and automated theorem proving. He received his Ph.D. in Computer Science from the University of Toronto in 2016, under the supervision of Azadeh Farzan. He received an NSF CAREER award (2020) and an honorable mention for the ACM SIGPLAN John C. Reynolds Doctoral Dissertation Award (2017).
Tom Reps:
Thomas Reps is the J. Barkley Rosser Professor & Rajiv and Ritu Batra Chair in the Computer Sciences Department of the University of Wisconsin, which he joined in 1985. He also co-founded GrammaTech, Inc., of which he was President from 1988-2019.
Reps is the author or co-author of four books and more than two hundred papers describing his research. His work has concerned a wide variety of topics, including dataflow analysis, abstract interpretation, program slicing, pointer analysis, model checking, computer security, code instrumentation, language-based program-development environments, the use of program profiling in software testing, software renovation, incremental algorithms, and attribute grammars.
Professor Reps received his Ph.D. in Computer Science from Cornell University in 1982. His Ph.D. dissertation received the 1983 ACM Doctoral Dissertation Award. Reps has also been the recipient of an NSF Presidential Young Investigator Award (1986), a Packard Fellowship (1988), a Humboldt Research Award (2000), and a Guggenheim Fellowship (2000). He is also an ACM Fellow (2005). In 2013, Reps was elected a foreign member of Academia Europaea. He received the ACM SIGPLAN Programming Languages Achievement Award for 2017.
Reps has held visiting positions at the Institut National de Recherche en Informatique et en Automatique (INRIA) in Rocquencourt, France (1982-83), the University of Copenhagen, Denmark (1993-94), the Consiglio Nazionale delle Ricerche in Pisa, Italy (2000-2001), and the Université Paris Diderot-Paris 7 (2007-2008).
SuSLik: Synthesis of Safe Pointer-Manipulating Programs
Nadia Polikarpova, University of California San Diego
Date: July 24
Abstract:
SuSLik is a program synthesizer that generates provably safe pointer-manipulating programs automatically from high-level specifications. More precisely, the input to SuSLik is a pair of assertions in separation logic, which describe what the heap looks like before and after executing the program. Using only this information, SuSLik is able to synthesize a wide range of operations on linked data structures, such as singly- and doubly-linked lists, binary trees, and rose trees.
In this tutorial you will get hands-on experience with SuSLik (bring your laptops!) and learn how synthesis is made possible by a novel proof system we call synthetic separation logic. Experience with separation logic and program synthesis is helpful but not required.
Bio: Nadia Polikarpova is an assistant professor at UC San Diego. She received her Ph.D. in Computer Science from ETH Zurich in 2014, and then spent a couple of years as a postdoctoral researcher at MIT. Nadia’s research interests are in program synthesis, program verification, and type systems. She is a 2020 Sloan Fellow, and a recipient of the 2020 NSF Career Award and the 2020 Intel Rising Stars Award.