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

University Of Washington, Seattle WA

Investigators

Abstract

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.