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

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

• 批准号: 2219863
• 负责人: Ratul Mahajan
• 金额: $ 37.5万
• 依托单位: University of Washington
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2022
• 资助国家: 美国
• 起止时间: 2022-10-01 至 2025-09-30
• 项目状态: 未结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=2219863&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.

计算机网络将用户连接到银行账户、在线商务、政府信息、社交媒体和其他云服务。它们对于现代商业和日常生活至关重要。然而，管理此类网络非常困难且容易出错。结果，破坏性的停电事件频繁发生，导致从食品配送到飞机航班再到关键信息服务的所有服务都被关闭。该研究项目开发了新技术，用于验证现代计算机网络的关键组件（数据平面），传统上仅用于转发流量，但越来越多地用于实现复杂的网络控制逻辑和下一代应用。正在开发的验证工具将在部署这些配置之前以及执行这些配置时检查网络配置，从而使网络更加可靠，并防止未来发生许多中断。该研究项目还为各类学生提供教育机会，教授他们网络和形式验证方法应用方面的关键技能。在可编程网络交换机和可编程网络接口卡 (NIC) 最新发展的推动下，工业计算机网络的数据平面变得高度动态，不仅可以转发流量，还可以实现网络控制逻辑，以适应不断变化的网络条件。拟议研究的目标是通过可以正式指定和验证网络范围行为的工具，使这些新网络更加可靠。这些规范使用事件的通用语言以统一的方式表示数据平面活动（例如，数据包到达）、控制平面消息（例如，路由公告）和应用层事件（例如，缓存条目的安装）。验证这些规范的验证技术结合使用静态和动态技术。静态验证在部署网络程序更改之前捕获错误，而动态验证则通过从高级规范综合的监视器检查静态假设是否成立，弥合扩展差距并提供深度防御。该奖项反映了 NSF 的法定使命，并通过使用基金会的智力优点和更广泛的影响审查标准进行评估，被认为值得支持。