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

网络和电信基础设施依赖于许多不同的网络协议，这些协议相互作用以提供通信服务。考虑到网络协议的数量和复杂性、不同的异构系统以及必须适应的各种管理策略，创建支持电信和Internet的软件本质上是困难的。这种复杂性大大增加了实现错误的可能性，这可能导致网络和安全漏洞（例如，广为人知的Heartbleed bug）。该项目将通过创建一种新的编程语言来解决这些问题，该语言通过一种按结构正确的编程风格来支持网络协议的综合及其相应的堆栈。该研究项目将研究新的转换方法和工具，用于设计、分析、构建、验证、配置和部署可证明正确、安全和高效的网络系统，这些方法和工具植根于系统编程语言的风格和理论。具体目标包括(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.