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

计算机网络将用户连接到银行账户、在线商务、有关政府的信息、社交媒体和其他云服务。它们对现代商业和日常生活都是必不可少的。然而，管理这样的网络是困难的，而且容易出错。其结果是，从食品运送到飞机航班再到关键信息服务的破坏性停电事件屡见不鲜。该研究项目开发了新技术，用于验证现代计算机网络的关键组件-其数据平面-传统上仅用于转发流量，但越来越多地用于实现复杂的网络控制逻辑和下一代应用。正在开发的验证工具将在部署这些配置之前检查网络配置，并在执行这些配置时检查网络配置，从而使网络更可靠，并防止未来发生多次停电。该研究项目还为各类学生提供教育机会，向他们传授联网和正式验证方法应用方面的关键技能。在可编程网络交换机和可编程网络接口卡(NIC)最近发展的推动下，工业计算机网络的数据平面正变得高度动态，不仅允许它们转发流量，而且还可以实现能够根据不断变化的网络条件进行调整的网络控制逻辑。拟议研究的目标是通过可正式指定和验证网络范围行为的工具，使这些新网络更加可靠。这些规范使用事件的公共语言来以统一的方式表示数据平面活动(例如，分组到达)、控制平面消息(例如，路由通告)和应用层事件(例如，高速缓存条目的安装)。验证这些规范的验证技术使用静态和动态技术相结合。静态验证在部署网络程序更改之前捕获错误，而动态验证通过从高级规范合成的监视器检查静态假设是否成立，弥合扩展差距，并提供深入的防御。该奖项反映了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.