如何避免数十亿美元的错误：使用SafeP4进行类型安全数据平面编程
How to Avoid Making a Billion-Dollar Mistake: Type-Safe Data Plane Programming with SafeP4
摘要：
P4程序设计语言提供了高级的声明性抽象，将软件的灵活性带到了网络领域。不幸的是，用于在P4中表示分组数据的主要抽象，即报头类型，缺乏基本的安全保证。在过去的几年里，越来越多的程序的经验表明了不安全方法的风险，这通常会导致微妙的软件错误。本文提出了SafeP 4，可编程数据平面，其中所有的数据包数据都保证有一个明确的意义，并满足基本的安全保障，特定于域的语言。我们装备SafeP 4的正式语义和静态类型系统，静态保证头的有效性-一个共同的安全漏洞来源，根据我们对现实世界的P4程序的分析。静态地确保头的有效性是具有挑战性的，因为有效头的集合可以在运行时修改，使其成为动态程序属性。我们的类型系统通过使用一种路径敏感的推理来实现静态安全，这种推理可以跟踪来自条件语句、路由表和控制平面的动态信息。我们的评估表明，SafeP 4的类型系统可以有效地消除常见的故障，在许多现实世界的程序。
英文摘要：
The P4 programming language offers high-level, declarative abstractions that bring the flexibility of software to the domain of networking. Unfortunately, the main abstraction used to represent packet data in P4, namely header types, lacks basic safety guarantees. Over the last few years, experience with an increasing number of programs has shown the risks of the unsafe approach, which often leads to subtle software bugs. This paper proposes SafeP4, a domain-specific language for programmable data planes in which all packet data is guaranteed to have a well-defined meaning and satisfy essential safety guarantees. We equip SafeP4 with a formal semantics and a static type system that statically guarantees header validity---a common source of safety bugs according to our analysis of real-world P4 programs. Statically ensuring header validity is challenging because the set of valid headers can be modified at runtime, making it a dynamic program property. Our type system achieves static safety by using a form of path-sensitive reasoning that tracks dynamic information from conditional statements, routing tables, and the control plane. Our evaluation shows that SafeP4's type system can effectively eliminate common failures in many real-world programs.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
