NeTS: Small: Collaborative Research: Tools for Design and Analysis of Provably Correct Networking Systems

点击翻译按钮获取中文摘要

Networking and telecommunications infrastructure relies on many different network protocols which interact to provide communication services. Software that enables telecommunications and the Internet is inherently difficult to create, given the number and complexity of network protocols, diverse heterogeneous systems, and various administrative policies that must be accommodated. This complexity significantly increases the likelihood of implementation errors, which can cause network and security vulnerabilities (e.g., the well-publicized Heartbleed bug). The project will address these issues through the creation of a new programming language that supports the synthesis of network protocols and their corresponding stack through a correct-by-construction style of programming.This research project will investigate new transformational methods and tools for the design, analysis, construction, verification, configuration, and deployment of provably correct, safe, and efficient networking systems, rooted in the style and theory of systems programming languages. Specific objectives include (i) the investigation and analysis of abstractions present in the message layer, state machine, system interfaces, and configuration tools of network protocols, and (ii) the reification of these abstractions in a new systems programming language that supports the definition of provably correct and efficient communication stacks.The project entails the analysis of software and hardware abstractions in modern networking and communication systems in order to support the design of programming language features. The project will identify correct by construction techniques that enable the design and synthesis of efficient systems that are immune to broad classes of vulnerabilities based on common programmer mistakes. Furthermore, the project will produce a language, compiler and runtime system accessible to a large community of researchers and engineers without requiring specialized expertise in formal methods.This project will contribute to understanding the foundation of the design of provably correct and secure computer and networking systems. The methodology developed in the course of this project will facilitate rapid development of vulnerability-free systems and will greatly benefit researchers, industry developers, and educators. The project's results will help improve networking system safety, security, and attack resilience. The project will make a significant contribution to the broader areas of axiomatic programming, programming methodologies, and formal methods. The project's results, as well as the developed models, testbeds, and software, will be disseminated to the research community and networking industry under an open source license.