CNS Core: Small: Test Framework for Easy and Effective Use of Network Verification

CNS Core：小型：轻松有效地使用网络验证的测试框架

• 批准号: 2007073
• 负责人: Ratul Mahajan
• 金额: $ 50万
• 依托单位: University of Washington
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2020
• 资助国家: 美国
• 起止时间: 2020-10-01 至 2024-09-30
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=2007073&HistoricalAwards=false
• 关键词: CNS; Core; Small; Test; Framework

As more people, devices, and services connect to the Internet, computer networks continue to increase in scale and complexity, which then leads to frequent outages and security breaches. In recent years, formal modeling and analysis has emerged as a promising approach to eliminate a broad class of network incidents. However, today, this approach is difficult to use and provides no feedback on how well it is being employed or the degree of protection it provides. This project aims to develop methods and metrics that enable easy and effective use of formal network analysis. It will develop a test framework which network engineers can use to easily specify correctness conditions for their networks and quantify how effectively the network is being tested. Consistent with NSF’s mission, these capabilities will help secure and fortify computer networks, which have become an integral part of modern society and business.At a high-level, the project will develop capabilities similar to those in test frameworks for software. However, networks are different from software, and the project will thus need to develop new domain-specific methods and metrics. Key areas of investigation include 1) an operational model for networks that can provide a basis for scientifically measuring test coverage; 2) coverage metrics that quantify how well different aspects of the network are being evaluated by a suite of tests; 3) a high-level language to easily express network invariants and facilitate coverage computation; and 4) a practical system that embeds these concepts and integrates with existing network verification tools to make formal analysis accessible to average network engineers. The work will be informed by close collaboration with industry and networks engineers that are either already using formal network analysis or motivated to do so.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.

随着越来越多的人、设备和服务连接到互联网，计算机网络的规模和复杂性不断增加，从而导致频繁的停机和安全漏洞。近年来，形式化建模和分析已成为消除各类网络事件的一种很有前途的方法。然而，今天，这种方法很难使用，而且没有提供任何关于它的使用情况或提供的保护程度的反馈。该项目旨在开发能够轻松有效地使用正式网络分析的方法和指标。它将开发一个测试框架，网络工程师可以使用该框架轻松地为他们的网络指定正确性条件，并量化网络测试的效率。与NSF的使命一致，这些能力将帮助保护和加强计算机网络，计算机网络已经成为现代社会和企业不可或缺的一部分。在高层次上，该项目将开发类似于软件测试框架中的能力。然而，网络不同于软件，因此该项目将需要开发新的特定于领域的方法和指标。主要研究领域包括：1)可以为科学地测量测试覆盖提供基础的网络操作模型；2)量化网络不同方面被一套测试评估得有多好的覆盖度量；3)易于表达网络不变量和促进覆盖计算的高级语言；以及4)嵌入这些概念并与现有网络验证工具集成以使一般网络工程师能够访问形式分析的实用系统。这项工作将通过与已经使用正式网络分析或有动机这样做的行业和网络工程师的密切合作来了解。该奖项反映了NSF的法定使命，并通过使用基金会的智力优势和更广泛的影响审查标准进行评估，被认为值得支持。