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

FMITF：第一轨：Petr4：可编程网络的正式基础

• 批准号: 1918396
• 负责人: John Foster
• 金额: $ 75万
• 依托单位: Cornell University
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2019
• 资助国家: 美国
• 起止时间: 2019-10-01 至 2024-09-30
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1918396&HistoricalAwards=false
• 关键词: FMitF; Track; Petr4; Formal; Foundations

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.

如今，大多数网络不是通过遵守精确的形式规格而是通过构建可容忍与正确行为偏差的实现来实现鲁棒性。但是，随着网络的规模和复杂性的增长，这些偏差引起的故障频率也增加了，从而对正式指定和验证网络行为的技术产生了新的兴趣。 PETR4（“ Petra”）项目的目标是通过为在网络设备（例如Internet路由器）上执行的程序开发精确的正式语义来建立新的网络基础。该项目的新颖性在于将基于编程的语言技术应用于新兴领域并构建经过验证的软件工具，例如编译器，该编译器生成了保证可以正确实施给定源程序的语义的代码。该项目的影响是开发开源软件，与行业合作伙伴进行技术转移，并为旨在从代表性不足的组中的本科生设计材料，在技术层面上，该项目将重点介绍四个独特的研究力量：（1）为P4编程语言开发一种正式的语言，以实现数学定义和伴随的均一代; （2）构建经过验证的编译器从P4到EBPF，该语言用于在Linux内核中表达自定义数据包处理； （3）研究新的控制平面API，足以捕获关键不变性并促进控制应用的正确组成； （4）开发可执行协议实现的库，该库可以组装到模块化的Internet路由器中。该项目将由一个跨学科研究团队指导，在正式方法和网络方面具有专业知识，并寻求不仅为网络建立新的基础，而且还可以作为跟进努力的催化剂，以促进网络堆栈的较高层次。该奖项反映了NSF的法定任务，并通过评估基金会的智力效果，反映了NSF的法定任务，并受到评估。

项目成果

Leapfrog: certified equivalence for protocol parsers

• DOI: 10.1145/3519939.3523715
• 发表时间: 2022-05
• 期刊: Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation
• 作者: Ryan Doenges;Tobias Kapp'e;J. Sarracino;Nate Foster;Greg Morrisett

P4Cub: A Little Language for Big Routers

P4Cub：大型路由器的小语言

• DOI: 10.1145/3573105.3575670
• 发表时间: 2023
• 期刊: ACM
• 作者: Peterson, Rudy;Campbell, Eric Hayden;Chen, John;Isak, Natalie;Shyu, Calvin;Doenges, Ryan;Ataei, Parisa;Foster, Nate
• 通讯作者: Foster, Nate

Petr4: formal foundations for p4 data planes

Petr4：p4 数据平面的正式基础

• DOI: 10.1145/3434322
• 发表时间: 2021
• 期刊: Proceedings of the ACM on Programming Languages
• 作者: Doenges, Ryan;Arashloo, Mina Tahmasbi;Bautista, Santiago;Chang, Alexander;Ni, Newton;Parkinson, Samwise;Peterson, Rudy;Solko-Breslin, Alaia;Xu, Amanda;Foster, Nate
• 通讯作者: Foster, Nate

Hydra: Effective Runtime Network Verification

• DOI: 10.1145/3603269.3604856
• 发表时间: 2023-09
• 期刊: Proceedings of the ACM SIGCOMM 2023 Conference
• 作者: Sundararajan Renganathan;Benny Rubin;Hyojoon Kim;Pier Luigi Ventre;C. Cascone;Daniele Moro;Charles Chan;N. McKeown;Nate Foster