论文标题
P4BID：P4中的信息流控制
P4BID: Information Flow Control in P4
论文作者
论文摘要
现代可编程网络交换机可以使用高效的数据包处理硬件实现自定义应用程序，并且编程语言P4提供了用于编程此类交换机的高级构造。速度和可编程性的提高激发了DataPlane编程中的研究，其中许多复杂的功能，例如键值商店和负载平衡器，都可以在网络交换机中完全实现。但是，DataPlane程序可能会遭受网络交换机中传统上未发现的新型安全错误。 为了解决此问题，我们为P4提供了一个新的信息流控制类型系统。我们在最近提供的P4核心版本中对类型系统进行了形式化，我们证明了一个合理的定理：良好的程序满足了不干预。我们还将我们的类型系统在工具P4BID中实现，该工具扩展了P4C编译器（最新版本的P4的参考编译器）中的类型检查器。我们提出了一些案例研究，表明网络中的自然安全性，完整性和隔离性能可以通过非干预来捕获，我们的类型系统可以在证明正确的程序时检测到对这些属性的侵犯。
Modern programmable network switches can implement custom applications using efficient packet processing hardware, and the programming language P4 provides high-level constructs to program such switches. The increase in speed and programmability has inspired research in dataplane programming, where many complex functionalities, e.g., key-value stores and load balancers, can be implemented entirely in network switches. However, dataplane programs may suffer from novel security errors that are not traditionally found in network switches. To address this issue, we present a new information-flow control type system for P4. We formalize our type system in a recently-proposed core version of P4, and we prove a soundness theorem: well-typed programs satisfy non-interference. We also implement our type system in a tool, P4bid, which extends the type checker in the p4c compiler, the reference compiler for the latest version of P4. We present several case studies showing that natural security, integrity, and isolation properties in networks can be captured by non-interference, and our type system can detect violations of these properties while certifying correct programs.
