MatchBox: A Semantic Foundation for Data Plane Portability
This program is tentative and subject to change.
Match-action tables are the core abstraction underlying network packet-processing systems, from fixed-function switches to eBPF-based software dataplanes. However, their concrete syntax and semantics vary widely across programming environments, reflecting differences in hardware generations, engineering practices, and vendor design choices. This syntactic and semantic variation renders portability of match-action tables across environments a persistent challenge. This paper presents \textsc{MatchBox}, a system for translating match-action tables across heterogeneous environments. At its core is the \emph{Match Algebra}, a compositional formalism for concisely and declaratively expressing transformations on match-action tables. To ensure unambiguous semantics, \textsc{MatchBox} introduces a static type system based on \emph{guarded functional dependencies (GFDs)} that guarantees that every well-typed Match Algebra expression denotes a well-defined function. From such specifications, the \textsc{MatchBox} compiler efficiently computes compact target tables that are semantically faithful. Across case studies in programmable switches, multi-cloud firewalls, and eBPF systems, \textsc{MatchBox} enables concise, declarative portability specifications and realizes them as compact target tables.