一句话：提出 MatchBox，以 Match Algebra 与 GFD 类型系统实现异构匹配-动作表的可移植翻译。
匹配-动作表是网络分组处理的核心抽象，但其语法与语义因硬件代际、工程实践和厂商选择而在固定功能交换机、eBPF 软件数据平面等环境中差异巨大，造成可移植性难题。本文提出 MatchBox，用于在异构环境间翻译匹配-动作表。其核心是可组合的 Match Algebra，以声明式方式简洁表达表变换；为保证语义无歧义，MatchBox 引入基于受保护函数依赖（GFD）的静态类型系统，确保每个良类型表达式都表示良定义函数。编译器据此高效计算紧凑且语义忠实的目标表。在可编程交换机、多云防火墙与 eBPF 系统的案例研究中，MatchBox 支持简洁的声明式可移植性规约并生成紧凑目标表。
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 MatchBox, a system for translating match-action tables across heterogeneous environments. At its core is the Match Algebra , a compositional formalism for concisely and declaratively expressing transformations on match-action tables. To ensure unambiguous semantics, MatchBox introduces a static type system based on guarded functional dependencies (GFDs) that guarantees that every well-typed Match Algebra expression denotes a well-defined function. From such specifications, the MatchBox compiler efficiently computes compact target tables that are semantically faithful. Across case studies in programmable switches, multi-cloud firewalls, and eBPF systems, MatchBox enables concise, declarative portability specifications and realizes them as compact target tables.
@article{CampbellZSAD26,
title = {MatchBox: A Semantic Foundation for Data Plane Portability},
author = {Eric Hayden Campbell and Robert Zhang and Divyanshu Saxena and Aditya Akella and Işıl Dillig},
journal = {Proceedings of the ACM on Programming Languages},
volume = {10},
number = {PLDI},
year = {2026},
doi = {10.1145/3808277}
}