Formal Foundations of Software Defined Networks

9 November 2020 - Madrid, Spain

Held in conjunction with the VI IEEE Conference on Network Function Virtualization and Software Defined Networks

New!

Prerecorded talks are now available!

Technical Focus and Motivation

There are several contemporary examples of network failures, particularly in the domain of SDNs, that led to substantial loss for businesses. Formal approaches have been proposed to provide a foundational approach to addressing such issues through correct-by-design construction, specification, and verification of SDN programs. Formal methods are promised to address performance, reliability, and security issues of SDNs using the rigour provided by their underlying mathematics. Hence, formal specification and verification of Network Functions Virtualization (NFV) and Software Defined Networks (SDN) have been gaining momentum in recent years. The focus of this workshop is on formal methods aimed to enable a formal specification and verification of SDNs and NFVs. The topics of interest include, but are not restricted to:

  • foundations (including formal semantics of) programming languages,
  • formal specification languages,
  • formal verification techniques,
  • synthesis and correct-by-construction methods, and
  • testing, debugging, monitoring and other forms of non-exhaustive validation and verification

Note that this workshop has no proceedings.

Motivational Speakers

Jennifer Rexford

Closing the Loop: Network Control in the Data Plane

Abstract

The proliferation of communication services that we depend on every day makes managing computer networks more important than ever. The increasing security, availability, and performance demands of these services suggest that these network-management problems must be solved in real time and inside the network. In this new era, network management requires a fundamentally new approach. Instead of performing offline analysis of network traces, future networks need to make real-time, closed-loop decisions to block unwanted traffic, to reroute traffic to avoid congestion, and more. This talk explores how to bring together network measurement, analysis, and control, by leveraging recent advances in programmable network devices and the P4 programming language (www.p4.org). We present several example network "apps" that detect and fix performance and security problems, while still processing packets at line rate in high-speed switches with limited memory. We also discuss our deployment experience with network telemetry P4 applications using Barefoot Tofino switches in the Princeton campus network.

Bio

Jennifer joined the Computer Science Department at Princeton University in February 2005 after eight and a half years at AT&T Research. Her research focuses on Internet routing, network measurement, and network management, with the larger goal of making data networks easier to design, understand, and manage. Jennifer is co-author of the book Web Protocols and Practice: HTTP/1.1, Networking Protocols, Caching, and Traffic Measurement (Addison-Wesley, May 2001) and co-editor of She's an Engineer? Princeton Alumnae Reflect (Princeton University, 1993, see recent talk about the book). Jennifer served as the chair of ACM SIGCOMM from 2003 to 2007, and has served on the ACM Council, the board of the Computing Research Association, the advisory council of the Computer and Information Science and Engineering directorate at NSF, and the Computing Community Consortium. She received her BSE degree in electrical engineering from Princeton University in 1991, and her MSE and PhD degrees in computer science and electrical engineering from the University of Michigan in 1993 and 1996, respectively. She was the winner of ACM's Grace Murray Hopper Award for outstanding young computer professional of the year for 2004.

Nikolaj Bjørner

SpecOps: Infusing specifications and formal tools in Azure cloud operations

Abstract

The talk outlines past and present interactions between Microsoft Research and Azure Networking around formal methods tools for harnessing cloud operations. Many of the tools are presently combined in the Network Change Verification System, which gates data-center deployments. NCVS relies on underlying tools CrystalBall, the Network Logic Solver, Z3, Spock, and Zen for specification, emulation, simulation, and validation. We use NCVS as an exemplar of use of formal methods in Ops scenarios, that we call SpecOps.

Bio

Nikolaj Bjørner works around the state-of-the-art SMT constraint solver Z3. Z3 was developed with Leonardo de Moura, Lev Nachmanson and Christoph Wintersteiger. Z3 is used for program verification, test case generation among several applications. Z3 received the 2015 ACM SIGPLAN Software System award and most influential tool paper in the first 20 years of TACAS. He and Leonardo de Moura received the Herbrand Award at CADE 2019, in recognition of numerous and important contributions to SMT solving, including its theory, implementation, and application to a wide range of academic and industrial needs. He and Karthick Jayaraman created the SecGuru tool that is used to validate firewalls and routing configurations for Microsoft Azure and George Varghese introduced me the networking. Until 2006, he was in the Core File Systems group where he designed and implemented the core of DFS-R which is included as part of Windows Server 2003 R2, Sharing Folders and Meetings Space. He also designed some of the chunking utilities used in the remote differential compression protocol RDC.

Paola Grosso

Putting the networks users in charge:  how can P4 help?

Abstract

Enhanced telemetry is one of areas where P4 is expected to open up new possibilities for increased insight in the way traffic flows, and to use this knowledge to steer and manage traffic flows. Is P4 a tool to make the Internet more transparent and increase trust from users? In this talk I will present our recent P4 work in the areas of user control and user verification of network paths. I will address the implications of P4 use towards a trusted Internet.

Bio

Dr. Paola Grosso is associate professor at the University of Amsterdam where she leads the Multiscale Networked Systems research group (mns-research.nl). Her research interests lie in the creation of sustainable and secure e-Infrastructures, relying on the provisioning and design of programmable networks. She carries out this work supported by several national research projects, such as Research on Networks, DL4LD, SecConNet and a number of EU-funded international projects FED4FIRE+, GN4 and ENVRIPLUS (H2020).  She contributes to the Dutch initiative 2STiC (2stic.nl) building a nationwide P4 testbed for experimentation towards the future internet.

Contributed Talks

David Walker

NV: A Platform for Modelling and Verifying Network Configurations

Abstract

Router configuration languages like those provided by CISCO, Juniper and other vendors are immensely complicated, with hundreds of commands and endless documentation. Building tools for analyzing such configurations directly is challenging and time consuming due to this complexity, especially when protocol transformations or abstractions are needed to improve analysis performance. In this talk, we will describe the design and implementation of NV, a functional language with a simple, small, orthogonal and compositional set of constructs that suffice to model the semantics and configuration of common network protocols. We have built several analysis tools for NV, including both compiled and interpreted mtBDD-based network simulators, an SMT-based verifier, and a network compression tool. Several of these tools outperform prior state-of-the-art tools in the same class thanks in part to the ease of applying a series of optimizing transformations over our intermediate language. We also have a translation tool that converts source-level configurations for a number of common protocols and configuration features into NV automatically.
This is joint work with Nick Giannarakis, Devon Loehr and Ryan Beckett.

Bio

David Walker is a Professor of Computer Science at Princeton University. He received his B.Sc. from Queen's University, Canada in 1995 and his Ph.D. in Computer Science from Cornell University in 2001. His research interests include programming language theory, design and implementation of all kinds. Most recently, he has focused on topics at the intersection of programming languages, formal methods and networking. In doing so, he has contributed to the design of several new languages for programming networks, including Frenetic, Pyretic, NetKAT, P4, and Propane. He and his co-authors have also developed a suite of tools for network configuration verification. Over the course of his career, he and his co-authors have won a number of awards for research in both programming languages and networking, including awards for work at POPL 1998, PLDI 2007, NSDI 2013, SIGCOMM 2016 and PLDI 2020. In addition, he won an NSF Career award, an Alfred Sloan Fellowship, and the ACM SIGPLAN Robin Milner Young Researcher Award. He served as an associate editor for ACM TOPLAS from 2007-2015 and as the Program Chair for POPL 2015. He helped found ACM SIGPLAN CARES.

Nate Foster

Petr4: Formal Foundations for P4 Data Planes

Abstract

P4 is a domain-specific language for specifying the behavior of packet-processing systems. It is based on an elegant design with high-level abstractions, such as parsers and match action pipelines, which can be compiled to efficient implementations in hardware or software. Unfortunately, like many industrial languages, P4 lacks a formal foundation. The P4 specification is a 160-page document with a mixture of informal prose, graphical diagrams, and pseudocode. The reference compiler is complex, running to over 40KLoC of C++ code. Clearly neither of these artifacts is suitable for formal reasoning. This talk will introduce a new framework called Petr4 (pronounced "Petra"), that puts P4 on a solid foundation. Petr4 uses standard elements of the semantics engineering toolkit, namely type systems and operational semantics, to build a compositional semantics that assigns an unambiguous meaning to every P4 program. Petr4 is implemented as an OCaml prototype that has been validated against a suite of over 750 tests from the reference implementation. While developing Petr4, we discovered dozens of bugs in the language specification and the reference implementation, many of which have been fixed. Furthermore, we have used Petr4 to establish the soundness of P4’s type system, prove key properties such as termination, and formalize a language extension.

Bio

Nate Foster is an Associate Professor of Computer Science at Cornell University, a Principal Research Engineer at Barefoot Networks, an Intel Company. 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, and several paper and teaching awards.

Brighten Godfrey

Title: Software as a Network

Abstract

The networking community’s energy in recent years has focused on making networks and network operations more software-driven. But meanwhile, the applications running on network infrastructure are changing, too, and becoming more like a network. This talk will explore how these trends may open new demands and opportunities for networks, across all layers of the stack, with examples in network performance and in verifying self-driving network infrastructure.

Bio

Brighten Godfrey is an Associate Professor in the Department of Computer Science at the University of Illinois at Urbana-Champaign. He co-founded and served as CTO of network verification pioneer Veriflow, through its 2019 acquisition by VMware where he now serves as a Technical Director. He received his Ph.D. at UC Berkeley in 2009, and his B.S. at Carnegie Mellon University in 2002. His research interests lie in the design of networked systems and algorithms. He is a winner of the ACM SIGCOMM Rising Star Award, the Sloan Research Fellowship, the National Science Foundation CAREER Award, and multiple best paper awards.

Schedule (time zone UTC+1)

Welcome

16:00 - 16:10

Putting the networks users in charge: how can P4 help?

Recorded talk: Here

16:10 - 16:40

— Paola Grosso University of Amsterdam

NV: A Platform for Modelling and Verifying Network Configurations

Recorded talk: Here

16:40 - 16:55

— David Walker Princeton University

Break

16:55 - 17:00

Closing the Loop: Network Control in the Data Plane

Recorded talk: Here

17:00 - 17:30

— Jennifer Rexford Princeton University

Petr4: Formal Foundations for P4 Data Planes

Recorded talk: Here

17:30 - 17:45

— Nate Foster Cornell University

Break

17:45 - 17:50

Software as a Network

Recorded talk: Here

17:50 - 18:05

— Brighten Godfrey University of Illinois at Urbana-Champaign

SpecOps: Infusing specifications and formal tools in Azure cloud operations

Recorded talk (Talk available only for download): Here

18:05 - 18:35

— Nikolaj Bjørner Microsoft Research

Organizers

Georgiana Caltais

University of Konstanz

Hossein Hojjat

Tehran Institute for Advanced Studies (TeIAS)

Mohammad Mousavi

University of Leicester