P4BID: Information Flow Control in P4

TL;DR

This paper introduces P4BID, a type system for P4 that enforces information flow control, ensuring security properties like non-interference in programmable network switches.

Contribution

It formalizes a new type system for P4, proves its soundness, and implements it in a tool to detect security violations in dataplane programs.

Findings

Type system enforces security properties in P4 programs.

Tool detects security violations while certifying correct programs.

Case studies demonstrate practical applicability of the approach.

Abstract

Modern programmable network switches can implement custom applications using efficient packet processing hardware, and the programming language P4 provides high-level constructs to program such switches. The increase in speed and programmability has inspired research in dataplane programming, where many complex functionalities, e.g., key-value stores and load balancers, can be implemented entirely in network switches. However, dataplane programs may suffer from novel security errors that are not traditionally found in network switches. To address this issue, we present a new information-flow control type system for P4. We formalize our type system in a recently-proposed core version of P4, and we prove a soundness theorem: well-typed programs satisfy non-interference. We also implement our type system in a tool, P4bid, which extends the type checker in the p4c compiler, the reference compiler for the latest version of P4. We present several case studies showing that natural security, integrity, and isolation properties in networks can be captured by non-interference, and our type system can detect violations of these properties while certifying correct programs.