ACM SIGCOMM 2021 TUTORIAL: Introduction to Network Verification

Tutorial Program

The tutorial has an associated Slack channel for discussions. Click on the link below to visit it. If you're asked to sign in, use the workspace name "sigcomm.slack.com" to sign up or sign in.

Call For Participation

Network verification has become a "hot topic" in recent years, with a variety of papers on the topic published at conferences like SIGCOMM and NSDI each year. Some of these papers focus on applying verification techniques to new domains, while others develop new data structures and algorithms, and still others focus on usability.

However, it can be hard for outsiders and practitioners to make sense of the area, which relies on techniques from programming languages and formal verification. For example, what's the difference between relational verification and symbolic execution? When is it better to use an SMT solver versus a model checker? Where do interactive proof assistants come in? And how do you automate verification and make it scale to large networks?

This half-day tutorial will provide a comprehensive introduction to formal verification as applied to networks, using the concrete domain of P4 data planes to ground the discussion. Using the recently developed Petr4 framework [1], we will show how to answer a range of verification problems using a wide variety of techniques. At the end of the tutorial, we plan to have a brief panel with a mixture of invited speakers from the networking and formal methods community.

Outline

A rough outline follows:

• Introduction

  • Recent successes in network verification
  • Taxonomy of verification techniques
  • Introduction to P4 language and running example

• Symbolic Execution

  • Generating path conditions from a program
  • Solving constraints using an SMT solver
  • Using abstraction to scale verification

• Relational Verification

  • Encoding correctness properties using first-order formulas
  • Verifying relational properties using program logics
  • Algebraic program reasoning

• Certified Soware

  • Verifying program transformations (e.g., compilers, hypervisors, etc.)
  • Introduction to deductive verification using proof assistants

• Panel Discussion

  • How can we make verification tools more scalable?
  • Are there any ideas for overcoming usability challenges?
  • What role does program synthesis have to play?
  • What would be a "holy grail" result in network verification?

• Conclusion

  • Academic conferences to follow
  • Papers to read
  • Tools and frameworks to try out

Audience Expectations and Prerequisites

The primary goal of this tutorial is to demystify network verification. As such, we plan to make the material accessible to the SIGCOMM audience and will assume no background in formal methods, other than undergrad-level programming experience. We also do not require any special computer requirements other than network connectivity and (optionally) the ability to run a Linux VM. We will provide instructions on how to install all necessary soware on Linux, Windows, and Mac OS. In addition, we will provide a VM with all necessary soware pre-installed. Otherwise no special background or requirements are required.

Organizers

• Ryan Doenges

  Cornell University

  • Bio: Ryan Doenges is a PhD student at Cornell University studying software-defined networking from a programming languages point of view. Prior to Cornell he received a B.S. in Mathematics from the University of Washington, where he was advised by Zachary Tatlock.

• Mina Tahmasbi Arashloo

  Cornell University

  • Bio: Mina Tahmasbi Arashloo is a presidential postdoctoral fellow at the computer science department of Cornell University, working with Nate Foster and Rachit Agarwal. Her research focuses on software defined networks and programmable data planes. Prior to Cornell, she received her PhD degree at Princeton University advised by Jennifer Rexford, and her B.Sc degree from Sharif University of Technology.

• Tobias Kappé

  Cornell University

  • Bio: Tobias Kappé is a postdoctoral associate at Cornell University, working on automated verification of P4 parsers. His background is in formal verification based on Kleene algebra and automata theory, with a particular interest in equational reasoning and bisimulation-based methods. He earned his PhD at University College London, advised by Alexandra Silva and Fabio Zanasi.

• Nate Foster

  Cornell University

  • 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.

References

[1] Ryan Doenges, Mina Tahmasbi Arashloo, Santiago Bautista, Alexander Chang, Newton Ni, Samwise Parkinson, Rudy Peterson, Alaia Solko-Breslin, Amanda Xu, and Nate Foster. 2020. Petr4: Formal Foundations for P4 Data Planes. In POPL.