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

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

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.