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

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

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.