Dependently-typed data plane programming
Dependently-typed data plane programming
复制标题
依赖类型数据平面编程
DOI：
--
复制
发表时间：
2022
期刊：
影响因子：
--
通讯作者：
M. Mezini
中科院分区：
文献类型：
--
作者：
Matthias Eichholz;E. Campbell;Matthias Krebs;Nate Foster;M. Mezini
像P4这样的编程语言可以在软件中指定网络数据平面的行为。然而，随着网络中运行的应用程序越来越强大和复杂，故障的风险也在增加。因此，人们越来越认识到需要静态验证P4代码正确性的方法和工具，特别是当语言缺乏基本的安全保证时。类型系统是建立程序属性的轻量级和组合方式，但是可以使用简单类型系统证明的属性之间存在显著差距（例如，SafeP4）和那些可以使用成熟的验证工具（例如，p4v）。在本文中，我们通过开发P4的依赖类型版本，基于可判定的细化，来缩小这一差距。我们激励的设计，证明其类型系统的合理性，开发一个基于SMT的实现，目前的案例研究，说明其适用于各种数据平面程序。
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.
Petr4：p4 数据平面的正式基础
影响因子：
--
作者：
Doenges, Ryan;Arashloo, Mina Tahmasbi;Bautista, Santiago;Chang, Alexander;Ni, Newton;Parkinson, Samwise;Peterson, Rudy;Solko-Breslin, Alaia;Xu, Amanda;Foster, Nate
通讯作者：
Foster, Nate