P4K：P4的形式语义及其应用
P4K: A Formal Semantics of P4 and Applications
摘要：
可编程分组处理器和P4作为这种设备的程序设计语言已经获得了极大的兴趣，因为它们的灵活性使得能够快速开发以线速工作的各种应用。然而，这种灵活性，加上设备和网络的复杂性，增加了引入难以手动发现的细微错误的机会。更糟糕的是，这是一个bug可能造成灾难性后果的领域，但P4程序/网络的正式分析工具却缺失。我们认为，正式的分析工具必须基于一个正式的语义的目标语言，而不是在其非正式的规格说明。为此，我们提供了一个可执行的形式语义的P4语言的K框架。基于这种语义，K为P4提供了解释器和各种分析工具，包括符号模型检查器和演绎程序验证器。本文概述了我们的形式化的P4的K语义，以及我们在形式化过程中发现的几个P4语言设计问题。我们还讨论了K为P4程序员和网络管理员以及语言设计人员和编译器开发人员提供的工具所产生的一些应用，例如不可移植代码的检测，P4程序和网络的状态空间探索，使用符号执行的错误发现，数据平面验证，程序验证和翻译验证。
英文摘要：
Programmable packet processors and P4 as a programming language for such devices have gained significant interest, because their flexibility enables rapid development of a diverse set of applications that work at line rate. However, this flexibility, combined with the complexity of devices and networks, increases the chance of introducing subtle bugs that are hard to discover manually. Worse, this is a domain where bugs can have catastrophic consequences, yet formal analysis tools for P4 programs / networks are missing. We argue that formal analysis tools must be based on a formal semantics of the target language, rather than on its informal specification. To this end, we provide an executable formal semantics of the P4 language in the K framework. Based on this semantics, K provides an interpreter and various analysis tools including a symbolic model checker and a deductive program verifier for P4. This paper overviews our formal K semantics of P4, as well as several P4 language design issues that we found during our formalization process. We also discuss some applications resulting from the tools provided by K for P4 programmers and network administrators as well as language designers and compiler developers, such as detection of unportable code, state space exploration of P4 programs and of networks, bug finding using symbolic execution, data plane verification, program verification, and translation validation.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
