RINGS: Accelerating the NextG Protocols Definition to Code Generation with an Automatic and Secure Verification-Compilation Tool-Chain

蜂窝网络已经成为日常生活中不可分割的一部分。5G等新一代蜂窝网络基础设施变得更加复杂，其开发将需要更大的努力和更长的时间。为了减少蜂窝基础设施对外国供应商的依赖，从而提高国家信息框架的安全性，有必要促进新一代蜂窝网络开放源码和安全软件的快速开发。这些努力中的一个巨大挑战是如何根据不断变化的NextG协议标准快速生成安全的开源代码。该研究项目开发了一个自动、安全和可扩展的工具链，以加速将NextG协议文档转换为可执行代码。该项目利用了用于协议描述的形式语言、用于安全分析的形式验证和用于代码生成的程序综合等技术进步。这些组件紧密集成，以探索协议软件合成的激进和改变游戏规则的方法。研究的结果是一系列工具，从NextG文档开始，产生协议的I/O自动机表示，最后生成安全的开源代码。该奖项反映了NSF的法定使命，并通过使用基金会的知识价值和更广泛的影响审查标准进行评估，被认为值得支持。

Cellular networks have become an inseparable part of everyday lives. Newer generations of cellular network infrastructure such as the 5G have become more complicated, and their developments will take larger effort and longer time. In order to reduce the dependence of cellular infrastructure on foreign providers, and thus to improve the security of the national information framework, it is necessary to facilitate the rapid development of open-source and secure software for new generations of cellular networks. A big challenge in these efforts is how to quickly generate secure open-source code according to the changing NextG protocol standards. This research project develops an automatic, secure, and scalable tool-chain to accelerate the translation of NextG protocol documents into executable code.The project leverages technical advancements in formal language for protocol description, formal verification for security analysis, and program synthesis for code generation. These components are tightly integrated to explore a radical and game-changing approach to the protocol software synthesis. The output of the research is a sequence of tools that start with NextG documents, produce I/O Automata representation of the protocols, and finally generate secure open-source code. Formal security analysis is also conducted on the I/O Automata representation to identify and remove vulnerabilities.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.