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

网络和电信基础设施依赖于许多不同的网络协议，这些协议相互作用以提供通信服务。考虑到网络协议的数量和复杂性、不同的异类系统以及必须适应的各种管理策略，实现电信和互联网的软件本身就很难创建。这种复杂性大大增加了实现错误的可能性，这可能会导致网络和安全漏洞(例如，广为人知的心脏出血漏洞)。该项目将通过创建一种新的编程语言来解决这些问题，这种新的编程语言支持通过逐个构造的编程风格来合成网络协议及其相应的堆栈。该研究项目将研究新的转换方法和工具，用于扎根于系统编程语言的风格和理论，用于设计、分析、构造、验证、配置和部署被证明正确、安全和高效的网络系统。具体目标包括(I)调查和分析网络协议的消息层、状态机、系统接口和配置工具中存在的抽象，以及(Ii)将这些抽象具体化为一种新的系统编程语言，该语言支持可证明正确和有效的通信堆栈的定义。该项目需要分析现代网络和通信系统中的软件和硬件抽象，以支持编程语言特征的设计。该项目将通过构建技术来识别正确的，从而能够设计和合成高效的系统，这些系统不受基于常见程序员错误的广泛类别的漏洞的影响。此外，该项目将产生一个语言、编译器和运行时系统，可供大量研究人员和工程师使用，而不需要正规方法方面的专门知识。该项目将有助于理解可证明正确和安全的计算机和网络系统设计的基础。在该项目过程中开发的方法将促进无漏洞系统的快速开发，并将极大地惠及研究人员、行业开发人员和教育工作者。该项目的成果将有助于提高网络系统的安全性、安全性和攻击弹性。该项目将对公理编程、编程方法和形式化方法等更广泛的领域做出重大贡献。该项目的结果，以及开发的模型、试验台和软件，将在开放源码许可下向研究社区和网络行业传播。

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.