Collaborative Research: FMitF: Track I: Specifying and Verifying Network-wide Properties of Dynamic Data Planes

合作研究：FMitF：第一轨：指定和验证动态数据平面的网络范围属性

• 批准号: 2219862
• 负责人: David Walker
• 金额: $ 37.5万
• 依托单位: Princeton University
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2022
• 资助国家: 美国
• 起止时间: 2022-10-01 至 2025-09-30
• 项目状态: 未结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=2219862&HistoricalAwards=false
• 关键词: Collaborative; Research; FMitF; Track; Specifying

Computer networks connect users to bank accounts, online commerce, information about government, social media, and other cloud services. They are essential for modern business and everyday life. However, managing such networks is difficult and error-prone. As a result, damaging outages that have shut down everything from food deliveries to plane flights to critical information services occur all too frequently. This research project develops new technology for verification of a key component of modern computer networks---their data planes---which traditionally have been used just to forward traffic, but are increasingly used to implement complex network control logic and next-generation applications. The verification tools being developed will check network configurations both prior to deployment of those configurations, and also as those configurations execute, thereby making networks more reliable, and preventing many future outages before they can occur. This research project also provides educational opportunities for a diverse range of students, teaching them key skills in both networking and the application of formal verification methods. Spurred by the recent development of programmable network switches and programmable network interface cards (NICs), the data planes of industrial computer networks are becoming highly dynamic, allowing them not only to forward traffic but also to implement network control logic that can adjust to evolving network conditions. The goal of the proposed research is to make these new networks substantially more reliable via tools that can formally specify and verify network-wide behavior. These specifications use a common language of events to represent data plane activity (e.g., packet arrivals), control plane messages (e.g., routing announcements), and application layer events (e.g., installation of a cache entry) in a uniform way. The verification technology to validate these specifications uses a combination of static and dynamic techniques. Static verification catches bugs before network program changes are deployed, while dynamic verification, via monitors synthesized from high-level specifications, checks that static assumptions hold up, bridges scaling gaps, and provides defense in depth.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.

计算机网络将用户连接到银行帐户，在线商务，有关政府，社交媒体和其他云服务的信息。它们对于现代业务和日常生活至关重要。但是，管理此类网络非常困难且容易出错。结果，从食物运送到飞机航班再到关键信息服务的所有事物的破坏破坏都过于频繁。该研究项目开发了新技术，以验证现代计算机网络的关键组成部分 - 它们的数据平面 - 传统上仅用于转发流量，但越来越多地用于实施复杂的网络控制逻辑和下一代应用程序。正在开发的验证工具将在部署这些配置之前检查网络配置，并且随着这些配置执行的执行，从而使网络更加可靠，并在发生之前预防许多未来的中断。该研究项目还为各种学生提供教育机会，教给他们在网络和正式验证方法的应用方面的关键技能。在最近的可编程网络交换机和可编程网络接口卡（NICS）的最新开发中，工业计算机网络的数据平面正在变得高度动态，不仅可以转发流量，还可以实现可以适应网络条件的网络控制逻辑。拟议的研究的目的是通过可以正式指定和验证网络范围行为的工具使这些新网络更加可靠。这些规格使用事件的通用语言来表示数据平面活动（例如，数据包到达），控制平面消息（例如路由公告）和应用程序层事件（例如，以统一的方式安装缓存条目）。验证这些规格的验证技术结合了静态和动态技术。 Static verification catches bugs before network program changes are deployed, while dynamic verification, via monitors synthesized from high-level specifications, checks that static assumptions hold up, bridges scaling gaps, and provides defense in depth.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.