P4K: A Formal Semantics of P4 and Applications

TL;DR

This paper introduces an executable formal semantics of the P4 language using the K framework, enabling advanced analysis tools for verifying and debugging programmable network programs to prevent costly bugs.

Contribution

It provides the first formal, executable semantics of P4 in the K framework, along with analysis tools like model checking and symbolic execution for P4 programs.

Findings

Detection of unportable code in P4 programs

State space exploration of P4 networks

Bug finding through symbolic execution

Abstract

Programmable packet processors and P4 as a programming language for such devices have gained significant interest, because their flexibility enables rapid development of a diverse set of applications that work at line rate. However, this flexibility, combined with the complexity of devices and networks, increases the chance of introducing subtle bugs that are hard to discover manually. Worse, this is a domain where bugs can have catastrophic consequences, yet formal analysis tools for P4 programs / networks are missing. We argue that formal analysis tools must be based on a formal semantics of the target language, rather than on its informal specification. To this end, we provide an executable formal semantics of the P4 language in the K framework. Based on this semantics, K provides an interpreter and various analysis tools including a symbolic model checker and a deductive program verifier for P4. This paper overviews our formal K semantics of P4, as well as several P4 language design issues that we found during our formalization process. We also discuss some applications resulting from the tools provided by K for P4 programmers and network administrators as well as language designers and compiler developers, such as detection of unportable code, state space exploration of P4 programs and of networks, bug finding using symbolic execution, data plane verification, program verification, and translation validation.