NeTS: Medium: Foundations and Applications of Modular Verification of Networks

网络将我们与我们的在线服务连接起来——我们的银行、我们的同事和朋友、我们的工作、我们的学校、我们的旅行计划、我们的政府资源等等。因此，网络是关键的基础设施，任何停机时间不仅代价高昂，而且可能很危险。为了正常工作，网络需要配置为在计算机之间路由信息。不幸的是，这些配置既庞大又复杂，在维护它们时很容易出错。该项目的目标是开发新的算法和工具，以便在网络配置造成严重危害之前识别错误。更具体地说，该项目将探索将复杂的现代网络划分为更小的组件（即模块）的方法，以便进行独立但准确的分析。这样做将允许复杂的分析技术扩展到可以应用于世界上最大和最重要的网络的程度。本课题将推进传统网络控制平面模块化验证的理论与实践。模块化推理可以帮助网络运营商抽象出不必要的细节，定位网络漏洞，确认配置更新的有效性，并将验证扩展到任意大的网络。具体目标是：(1)发展新的理论基础，包括网络行为模型、有用的抽象和支持健全和高效模块化推理的表达性规范语言；（二）设计并实现模块化网络接口验证与综合的算法方法；(3)构建可靠的模块化网络管理系统，支持传统基础设施的迁移。可靠的网络是国家关键基础设施的重要组成部分。如果成功，这个项目产生的想法和产品将有助于保持基础设施的运行，并避免由于网络配置更新而导致的错误导致的中断。为了增加计算机科学教育的机会，该项目将遵循普林斯顿大学的“部门扩大参与计算”计划。特别是，该项目将支持本科生的研究机会。为了改善教育成果，该项目将开发关于正式方法的跨学科共享教材，用于本科和研究生阶段的课堂。项目产生的结果，包括开源代码、数据和报告，将通过https://www.cs.princeton.edu/~dpw/grants/nsf-modular-networks.html访问。这些产品将至少维持十年。该奖项反映了美国国家科学基金会的法定使命，并通过使用基金会的知识价值和更广泛的影响审查标准进行评估，被认为值得支持。

Networks connect us to our online services – our banks, our colleagues and friends, our work, our school, our travel plans, our government resources, and so much more. As such, networks are critical infrastructure, and any downtime is not only costly, but possibly dangerous. In order to function properly, networks need to be configured to route information between computers. Unfortunately, these configurations are large and complicated, and it is easy to make mistakes while maintaining them. The goal of this project is to develop new algorithms and tools to identify mistakes in network configurations before they cause serious harm. More specifically, the project will explore ways to divide complex modern networks into smaller components (i.e., modules) for separate but accurate analysis. Doing so will allow sophisticated analysis techniques to scale to the point they may be applied to the world’s largest and most important networks. This project will advance the theory and practice of modular verification of traditional network control planes. Modular reasoning can help network operators abstract away unnecessary details, localize network bugs, confirm the validity of configuration updates, and scale verification to arbitrarily-large networks. The specific goals are: (1) to develop new theoretical foundations, including models of network behavior, useful abstractions, and expressive specification languages that support sound and efficient modular reasoning; (2) to design and implement algorithmic methods for verification and synthesis of modular network interfaces; and (3) to build a system for reliable modular network management, with support for migration from traditional infrastructure.Reliable networks are an essential component of the nation’s critical infrastructure. If successful, the ideas and products produced by this project will help keep that infrastructure running and avoid outages resulting from bugs due to updates in network configurations. To increase access to education in computer science, the project will follow Princeton’s verified Departmental Broadening Participation in Computing plan. In particular, the project will support undergraduate research opportunities. To improve educational outcomes, the project will develop shared interdisciplinary educational materials on formal methods to be deployed in classes at the undergraduate and graduate levels.Results produced by the project including open source code, data, and reports will be accessible via https://www.cs.princeton.edu/~dpw/grants/nsf-modular-networks.html. These products will be maintained for at least a decade.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.