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

NetS：小型：协作研究：设计和分析可证明正确的网络系统的工具

• 批准号: 1423322
• 负责人: Alexander Sprintson
• 金额: $ 35.14万
• 依托单位: Texas A&M Engineering Experiment Station
• 依托单位国家: 美国
• 项目类别: Continuing Grant
• 财政年份: 2014
• 资助国家: 美国
• 起止时间: 2014-10-01 至 2018-09-30
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1423322&HistoricalAwards=false
• 关键词: NeTS; Small; Collaborative; Research; Tools

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.

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