Software-Defined Networking (SDN) significantly simplifies programming, reconfiguring, and optimizing network devices, such as switches and routers. The de facto standard for programmming 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 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_{\text{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.

翻译：软件定义网络（SDN）显著简化了网络设备（如交换机和路由器）的编程、重构与优化过程。P4语言已成为编程SDN设备的事实标准。然而，P4及更广泛的SDN的灵活性与强大功能也带来了重大风险。正如多家主流云服务商发生的故障所揭示，SDN程序中的错误可能导致网络可用性受损，使其陷入失效状态。本文重点研究通过标准化P4Runtime API与支持P4的网络设备交互的控制平面程序中出现的错误。尽管采用Google Protocol Buffers作为接口定义语言，但P4Runtime API的客户端仍易因操作失误引发灾难性故障。本文提出P4R-Type——一个面向Scala语言的新型验证型P4Runtime API，可对P4控制平面操作进行静态检查，从而排除P4表、允许动作及动作参数之间的不匹配问题。作为P4R-Type的形式化基础，我们提出$F_{\text{P4R}}$演算及其类型系统，确保类型良好的程序不会因执行无效P4Runtime操作而陷入停滞。通过3个案例研究，我们评估了P4R-Type的安全性与灵活性。据我们所知，这是首个将P4Runtime控制平面应用程序形式化，并建立确保P4Runtime操作正确性的类型规范的工作。