FMitF: Track I: Petr4: Formal Foundations for Programmable Networks

今天，大多数网络实现健壮性不是通过遵守精确的正式规范，而是通过构建能够容忍适度偏离正确行为的实现。但是，随着网络规模和复杂性的增长，由这些偏差引起的故障频率也在增加，这导致人们对正式指定和验证网络行为的技术产生了新的兴趣。Petr4（“petra”）项目的目标是通过为在网络设备（如Internet路由器）上执行的程序开发一种精确的形式化语义，为网络建立一个新的基础。该项目的新颖之处在于将基于编程语言的技术应用于新兴领域，并构建经过验证的软件工具，例如生成保证正确实现给定源程序语义的代码的编译器。该项目的影响包括开发开源软件，寻求与工业伙伴的技术转让，以及为面向代表性不足群体的大学生的外联讲习班设计材料。在技术层面上，该项目将侧重于四个不同的研究重点：(1)为P4编程语言开发形式化语义，作为一组数学定义和附带的参考实现实现；(2)构建一个经过验证的编译器，从P4到eBPF， eBPF是Linux内核中用于表达自定义包处理的语言；(3)研究新的控制平面api，这些api足够丰富，可以捕获关键不变量并促进控制应用程序的正确组合；(4)开发可执行协议实现库，该库可组装成模块化互联网路由器。该项目将由一个具有正式方法和网络专业知识的跨学科研究团队指导，并寻求不仅为网络开发新的基础，而且还作为后续努力的催化剂，目标是网络堆栈的更高层次。该奖项反映了美国国家科学基金会的法定使命，并通过使用基金会的知识价值和更广泛的影响审查标准进行评估，被认为值得支持。

Most networks today achieve robustness not by adhering to precise formal specifications but by building implementations that tolerate modest deviations from correct behavior. But as networks have grown in scale and complexity, the frequency of faults caused by these deviations has increased, leading to new interest in techniques for formally specifying and verifying network behavior. The goal of the Petr4 ("petra") project is to build a new foundation for networking by developing a precise, formal semantics for the programs that execute on network devices such as Internet routers. The project's novelties are in applying programming language-based techniques to an emerging area and building verified software tools, such as a compiler that generates code guaranteed to correctly implement the semantics of a given source program. The project's impacts are in developing open-source software, pursuing technology transfer with industry partners, and designing material for an outreach workshop aimed at undergraduates from under-represented groups.At a technical level, the project will focus on four distinct research thrusts: (1) Developing a formal semantics for the P4 Programming Language, realized as a set of mathematical definitions and an accompanying reference implementation; (2) Building a verified compiler from P4 to eBPF, the language used to express custom packet-processing in the Linux kernel; (3) Investigating new control-plane APIs that are rich enough to capture key invariants and facilitate correct composition of control applications; and (4) Developing a library of executable protocol implementations that can be assembled into a modular Internet router. The project will be guided by an interdisciplinary research team with expertise in both formal methods and networking, and seeks to not only develop a new foundation for networking, but also serve as a catalyst for follow-on efforts that target higher layers of the networking stack.This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.