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

NeTS：媒介：网络模块化验证的基础和应用

• 批准号: 2312539
• 负责人: David Walker
• 金额: $ 108.3万
• 依托单位: Princeton University
• 依托单位国家: 美国
• 项目类别: Continuing Grant
• 财政年份: 2023
• 资助国家: 美国
• 起止时间: 2023-10-01 至 2027-09-30
• 项目状态: 未结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=2312539&HistoricalAwards=false
• 关键词: NeTS; Medium; Foundations; Applications; Modular

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.

网络将我们连接到我们的在线服务 - 我们的银行，同事和朋友，我们的工作，我们的学校，我们的旅行计划，我们的政府资源等等。因此，网络是关键的基础设施，任何停机时间不仅昂贵，而且可能是危险的。为了正常运行，需要将网络配置为在计算机之间路由信息。不幸的是，这些配置很大且复杂，并且在维护它们的同时很容易犯错。该项目的目的是开发新的算法和工具，以在造成严重伤害之前识别网络配置中的错误。更具体地说，该项目将探索将复杂的现代网络分为较小的组件（即模块）进行单独但准确的分析的方法。这样做将使复杂的分析技术扩展到可能应用于世界上最大，最重要的网络。该项目将推动传统网络控制平面模块化验证的理论和实践。模块化推理可以帮助网络运营商抽象不必要的详细信息，本地化网络错误，确认配置更新的有效性以及将验证扩展到任意大型网络。具体目标是：（1）开发新的理论基础，包括网络行为的模型，有用的抽象和支持声音和有效模块化推理的表达性特定语言； （2）设计和实施算法方法，以验证和合成模块化网络接口； （3）为可靠的模块化网络管理构建系统，并支持从传统基础架构迁移。可靠的网络是国家关键基础架构的重要组成部分。如果成功，该项目产生的想法和产品将有助于保持基础架构运行，并避免由于网络配置中的更新而导致错误导致的中断。为了增加计算机科学中的教育机会，该项目将遵循普林斯顿验证的部门扩大计算计划的参与。特别是，该项目将支持本科研究机会。 To improve education 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.这些产品将至少十年维护。该奖项反映了NSF的法定任务，并通过使用基金会的知识分子优点和更广泛的影响评估标准来评估，以诚实的支持。