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

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

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.