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