一句话：提出基于可判定精化的依赖类型 P4 方言 Π4，为数据平面程序提供轻量级静态验证。
P4 等语言可在软件中规定网络数据平面行为，但语言缺少基本安全保证，复杂应用增加故障风险。现有简单类型系统（如 SafeP4）与完整验证工具（如 p4v）所能证明的性质之间存在明显鸿沟。本文提出 Π4：基于可判定精化的依赖类型版 P4，以轻量且组合的方式表达并静态检查数据平面程序性质。作者论证设计动机，证明类型系统可靠性，开发基于 SMT 的实现，并通过多个数据平面程序案例研究展示其适用性。结果表明 Π4 能缩小轻量类型检查与重量验证之间的表达力差距。
Programming languages like P4 enable specifying the behavior of network data planes in software. However, with increasingly powerful and complex applications running in the network, the risk of faults also increases. Hence, there is growing recognition of the need for methods and tools to statically verify the correctness of P4 code, especially as the language lacks basic safety guarantees. Type systems are a lightweight and compositional way to establish program properties, but there is a significant gap between the kinds of properties that can be proved using simple type systems (e.g., SafeP4) and those that can be obtained using full-blown verification tools (e.g., p4v). In this paper, we close this gap by developing Π4, a dependently-typed version of P4 based on decidable refinements. We motivate the design of Π4, prove the soundness of its type system, develop an SMT-based implementation, and present case studies that illustrate its applicability to a variety of data plane programs.
@article{paperbot1551,
title = {Dependently-typed data plane programming},
author = {Matthias Eichholz and Eric Hayden Campbell and Matthias Krebs and Nate Foster and Mira Mezini},
journal = {Proceedings of the ACM on Programming Languages},
volume = {6},
number = {POPL},
year = {2022},
doi = {10.1145/3498701}
}