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.
翻译:现代可编程网络开关可以使用高效的包处理硬件实施定制应用程序,而编程语言P4为程序开关提供了高层次的构造。速度和可编程性的提高激发了数据机编程的研究,许多复杂的功能,例如关键值仓库和负载平衡器,都可以完全在网络开关中实施。然而,数据机程序可能因网络开关中历来不见的新的安全错误而受到影响。为了解决这个问题,我们为P4提供了一个新的信息流控制类型系统。我们将我们的型号系统正式化为最近提出的P4核心版本,我们证明了一种健全的理论:类型良好的程序可以满足不干涉。我们还在一种工具P4bider中实施了我们的型号系统,该工具扩大了P4c编译器中的类型检查器,这是最新版本P4的参考汇编器。我们提出了几项案例研究,表明网络中的自然安全、完整性和隔离性能可以通过不干扰来捕捉到,我们的型号系统可以在验证正确程序时发现这些属性的违规情况。