蜂窝网络协议（如4G/5G）的规范文档通常以自然语言编写，安全分析师需要从这些非形式化描述中手工提取协议状态机，以进行安全分析和漏洞挖掘。这一过程极为耗时且容易出错，阻碍了大规模系统性安全评估。本文提出 Hermes，一个端到端框架，能够自动从自然语言编写的蜂窝网规格说明中生成形式化的有限状态机（FSM）模型。Hermes 首先开发了一个神经成分解析器 NEUTREX，用于处理与状态转换相关的文本，提取转换三元组：状态、条件和动作。接着，设计了一种领域特定语言（DSL），利用依赖解析树将这些转换组件转化为逻辑公式。最后，编译这些逻辑公式生成状态迁移，并组装为有限状态机。作者在 4G NAS、5G NAS 和 5G RRC 三个规范集上评估 Hermes，取得 81–87% 的总体准确率，大幅优于现有方法。基于提取出的模型，安全分析发现了 3 个新漏洞，确认了 4G/5G 规格中已有的 19 个攻击，并在商用 4G 基带中发现 7 处与规范的偏差。该工作展示了从自然语言规范到可分析形式模型的自动化路径，为协议安全测试和形式化验证提供了可扩展的工具支持。

该论文研究了LTE核心网络中的上行链路安全漏洞，特别是上下文完整性违反（Context Integrity Violations, CIV）问题。CIV是指未经认证或认证不当的用户设备（UE）修改其他用户内部状态的行为。以往研究主要集中在下行链路漏洞，而上行链路安全关注不足。作者提出了CITesting，这是首个系统性检测LTE核心网络中CIV的框架。CITesting通过探索多种过程链、测试广泛的信息元素（IE）、验证UE连接状态下的行为，并引入有状态的双UE控制测试来管理受害者UE状态，利用行为预言机在黑盒网络中检测上下文修改。该框架在四个LTE核心网实现（开源Open5GS、srsRAN，商业Amarisoft、Nokia）上进行了评估，经过后分析分别发现了29、22、16和59个不同的CIV。这些漏洞可实现远程攻击，包括UE脱离、IMSI暴露和存在检测攻击。与传统攻击模型（如伪基站）要求攻击者与受害者位于同一小区不同，本研究中攻击者仅需与受害者UE处于同一MME区域（远大于小区范围）。所有发现已负责任地披露，并向Amarisoft和Open5GS贡献了补丁。

本文针对虚假基站（FBS）检测领域面临的现实挑战展开研究。过去二十年来，由于获取商用FBS（C-FBS）设备存在巨大的财务和监管壁垒，研究者无法直接观察真实攻击行为，导致检测系统多基于自建原型进行设计与评估，可能遗漏实际攻击面的关键盲区。为此，作者提出Devilray——一种可重构、参考级的对抗基线模型，旨在系统性地探索现实对抗空间，识别现有检测方案中的盲点。研究通过首次对商用FBS进行学术分析，建立了经验性的事实基础，并扩展至3GPP标准允许的规范驱动操作变体。Devilray能够系统生成2592种可行且真实的FBS实例，覆盖广泛的操作可能性。利用Devilray，作者评估了七种代表性可获取FBS检测器，发现所有检测器均存在覆盖率缺口，这些盲点源于假设限制性的设计与评估方法。本工作提供了第一个基于真实行为和规范分析的强健对抗模型，使社区能够以严谨的方式开发和评估未来的检测机制。适合移动安全、蜂窝网络防御领域的研究者阅读。