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自动机表示，最后生成安全的开源代码。该奖项反映了NSF的法定使命，并通过使用基金会的知识价值和更广泛的影响审查标准进行评估，被认为值得支持。

项目成果

SE3: Sequential Equivalence Checking for Non-Cycle-Accurate Design Transformations †

SE3：非周期精确设计转换的顺序等价检查 †

• DOI: 10.1109/dac56929.2023.10247912
• 发表时间: 2023
• 期刊: 2023 60th ACM/IEEE Design Automation Conference (DAC)
• 作者: You Li;Guannan Zhao;Yunqi He;H. Zhou
• 通讯作者: H. Zhou

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

ObfusLock: An Efficient Obfuscated Locking Framework for Circuit IP Protection†

ObfusLock：用于电路 IP 保护的高效混淆锁定框架†

• 发表时间: 2023
• 期刊: Design, Automation and Test in Europe
• 作者: You Li;Guannan Zhao;Yunqi He;H. Zhou
• 通讯作者: H. Zhou

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