一句话：提出经过验证的 Scala P4Runtime API P4R-Type，通过静态检查与类型系统排除控制平面操作错误。
SDN 中 P4 设备控制平面程序容易因 P4Runtime API 调用错误而导致网络故障，即便使用 Protocol Buffers 作为接口定义语言，表、允许 action 与 action 参数之间的不匹配仍难以避免。论文提出 P4R-Type，一个面向 Scala 的经过验证的 P4Runtime API，对 P4 控制平面操作进行静态检查，排除 P4 表、允许 action 与 action 参数之间的不匹配。其形式基础是 F P4R 演算及其类型系统，保证良类型程序不会因发出非法 P4Runtime 操作而卡住。作者通过 3 个案例研究评估 P4R-Type 的安全性与灵活性，并称这是首个形式化 P4Runtime 控制平面应用及确保操作正确性的类型规则的工作。
Software-Defined Networking (SDN) significantly simplifies programming, reconfiguring, and optimizing network devices, such as switches and routers. The de facto standard for programming SDN devices is the P4 language. However, the flexibility and power of P4, and SDN more generally, gives rise to important risks. As a number of incidents at major cloud providers have shown, errors in SDN programs can compromise the availability of networks, leaving them in a non-functional state. The focus of this paper are errors in control-plane programs that interact with P4-enabled network devices via the standardized P4Runtime API. For clients of the P4Runtime API it is easy to make mistakes that may lead to catastrophic failures, despite the use of Google’s Protocol Buffers as an interface definition language. This paper proposes P4R-Type, a novel verified P4Runtime API for Scala that performs static checks for P4 control plane operations, ruling out mismatches between P4 tables, allowed actions, and action parameters. As a formal foundation of P4R-Type, we present the F P4R calculus and its typing system, which ensure that well-typed programs never get stuck by issuing invalid P4Runtime operations. We evaluate the safety and flexibility of P4R-Type with 3 case studies. To the best of our knowledge, this is the first work that formalises P4Runtime control plane applications, and a typing discipline ensuring the correctness of P4Runtime operations.
@article{paperbot1853,
title = {P4R-Type: A Verified API for P4 Control Plane Programs},
author = {Jens Kanstrup Larsen and Roberto Guanciale and Philipp Haller and Alceste Scalas},
journal = {Proceedings of the ACM on Programming Languages},
volume = {7},
number = {OOPSLA2},
year = {2023},
doi = {10.1145/3622866}
}