依赖类型的数据平面编程
摘要：使用类似P4编程语言的能够在软件中指定网络数据平面行为。然而，随着网络中运行的应用程序越来越强大和复杂，故障的风险也增加。因此，越来越多人认识到需要方法和工具来静态验证P4代码的正确性，特别是因为该语言缺乏基本的安全性保证。类型系统是一种轻量级和组合性的方式来建立程序属性，但是简单的类型系统（例如SafeP4）能够证明的属性种类与使用完整的验证工具（例如p4v）所能获得的种类之间存在重大差距。在本文中，我们通过开发基于可判定细化的$Pi$4，一个依赖类型的P4版本，来弥合这一差距。我们阐述了$Pi$4的设计动机，证明了其类型系统的正确性，开发了基于SMT的实现，并提供了案例研究，说明它适用于各种数据平面程序。
作者：Matthias Eichholz, Eric Hayden Campbell, Matthias Krebs, Nate Foster, Mira Mezini
论文ID：2206.03457
分类：Programming Languages
分类简称：cs.PL
提交时间：2022-06-08