Hermes:通过从自然语言规范合成有限状态机解锁蜂窝网络协议的安全分析
密码学与安全
2023-10-12 v2 人工智能
计算与语言
摘要
在本文中,我们提出 Hermes,一个从自然语言蜂窝规范自动生成形式化表示的端到端框架。我们首先开发了一个神经成分句法分析器 NEUTREX,用于处理与转移相关的文本并提取转移组件(即状态、条件和动作)。我们还设计了一种领域特定语言,通过利用依存句法树将这些转移组件翻译为逻辑公式。最后,我们编译这些逻辑公式以生成转移,并创建作为有限状态机的形式化模型。为展示 Hermes 的有效性,我们在 4G NAS、5G NAS 和 5G RRC 规范上评估它,获得了 81-87% 的总体准确率,相比最先进水平有显著提升。我们对提取模型的安全分析发现了 3 个新漏洞,并识别出 4G 和 5G 规范中的 19 个先前攻击,以及商用 4G 基带中的 7 个偏差。
引用
@article{arxiv.2310.04381,
title = {Hermes: Unlocking Security Analysis of Cellular Network Protocols by Synthesizing Finite State Machines from Natural Language Specifications},
author = {Abdullah Al Ishtiaq and Sarkar Snigdha Sarathi Das and Syed Md Mukit Rashid and Ali Ranjbar and Kai Tu and Tianwei Wu and Zhezheng Song and Weixuan Wang and Mujtahid Akon and Rui Zhang and Syed Rafiul Hussain},
journal= {arXiv preprint arXiv:2310.04381},
year = {2023}
}
备注
Accepted at USENIX Security 24