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

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

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.