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

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

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.