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

RINGS：利用自动安全的验证编译工具链加速 NextG 协议定义到代码生成

• 批准号: 2148177
• 负责人: Yan Chen
• 金额: $ 90万
• 依托单位: Northwestern University
• 依托单位国家: 美国
• 项目类别: Continuing Grant
• 财政年份: 2022
• 资助国家: 美国
• 起止时间: 2022-05-01 至 2025-04-30
• 项目状态: 未结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=2148177&HistoricalAwards=false
• 关键词: RINGS; Accelerating; NextG; Protocols; Definition

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.

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

项目成果

Discovering emergency call pitfalls for cellular networks with formal methods

使用形式化方法发现蜂窝网络的紧急呼叫陷阱

• DOI: 10.1145/3458864.3466625
• 发表时间: 2021
• 期刊: MobiSys 2021
• 作者: Hou, Kaiyu;Li, You;Yu, Yinbo;Chen, Yan;Zhou, Hai
• 通讯作者: Zhou, Hai

Global Attack and Remedy on IC-Specific Logic Encryption

IC专用逻辑加密的全球攻击和补救措施

• DOI: 10.1109/host54066.2022.9840128
• 发表时间: 2022
• 期刊: 2022 IEEE International Symposium on Hardware Oriented Security and Trust (HOST
• 作者: Rezaei, Amin;Hedayatipour, Ava;Sayadi, Hossein;Aliasgari, Mehrdad;Zhou, Hai
• 通讯作者: Zhou, Hai