Oct, 2023

Hermes：通过从自然语言规范中合成有限状态机解锁移动网络协议的安全分析

PDF
TL;DR该研究发表了 Hermes - 一个端到端框架，可自动从自然语言的细胞规范中生成形式表示。通过开发神经成分解析器 NEUTREX，将转换相关的文本处理并提取转换组件（即状态、条件和动作），并通过依赖解析树将这些转换组件转化为逻辑公式。最后，将这些逻辑公式编译成转换，并创建有限状态机的形式模型。通过在 4G NAS、5G NAS 和 5G RRC 规范上进行评估，Hermes 的整体准确率为 81-87％，这相对于现有技术是一项重大改进。所提取模型的安全分析揭示了 4G 和 5G 规范中的 3 个新的漏洞、19 个先前的攻击，以及商用 4G 基带中的 7 个偏差。
发现论文，激发创造
  • 从协议规范文档中提取有限状态机进行自动攻击合成

    本文提出了一种数据驱动、规则映射以及聚焦零样本学习的混合方法，从 RFC 文档中自动提取有限状态机，推广到了六种不同协议的 FSM 提取，并演示了对 RFC 中 TCP 和 DCCP 协议的攻击自动化合成。

    Feb, 2022

  • 从模糊到明确：NLP 辅助的 5G 规范抽象用于形式分析

    通过自然语言处理辅助方法，在协议设计中提供了一种将正式方法应用于宏大复杂规范和协议分析的高效流程，尤其适用于 5G 和下一代通信。

    Aug, 2023

  • 面向 NextG 协议形式验证的自动建模：一种多模态的跨向与自标注意力大语言模型方法

    利用 Auto-modeling of Formal Verification with Real-world Prompting for 5G and NextG protocols (AVRE) 系统，通过 Large Language Models（LLMs）将协议描述转换为依赖关系图和形式模型，实现了自动建模和验证，来验证通信协议的复杂性和可扩展性。与传统模型相比较，该系统在准确性和稳健性方面表现出优势，并首次基于自然语言处理的方法在设计文档中直接创建漏洞，取得了可扩展系统验证和验证方面的重大进展。

    Dec, 2023

  • 命名实体识别的神经网络结构

    本文介绍基于双向 LSTM 和条件随机场，以及基于转移的方法的两种新的神经网络模型，这些模型不依赖于领域特定的知识和语言。通过使用监督语料库和未标注语料库，字符表示和无监督的学习表示，这些模型在四种语言中实现了名词实体识别的最先进性能。

    Mar, 2016

  • 迈向 6G 的语义通信协议：从协议学习到以语言为导向的方法

    本文对数据驱动介质访问控制（MAC）协议进行了新颖的分类，分为三个级别：第一级 MAC，使用多智能体深度强化学习（MADRL）构建的面向任务的神经协议；第二级 MAC，通过将第一级 MAC 的输出转化为明确符号来开发神经网络导向的符号协议；第三级 MAC，利用大型语言模型（LLMs）和生成模型的语言导向的语义协议。通过这种分类，我们旨在探究每个级别的机遇和挑战，并从信息论和相关原理以及选定的案例研究中提供对数据驱动 MAC 协议的轨迹的见解，同时为未来的研究方向提供启示。

    Oct, 2023

  • 为无线通信规范信息合成调整基础模型

    该论文介绍了 NextGen Communications Copilot，这是一个用于综合无线通信规范信息的对话式人工智能工具，它包括了一个领域特定数据库、上下文提取器和反馈机制，通过从无线技术规范数据库中提取简明且与查询相关的上下文信息，以及专家反馈和数据贡献工具，得到了更相关和准确的答案，其平均 BLEU 分数和 BERTScore F1-measure 分别为 0.37 和 0.79，相比于像 ChatGPT 这样的最先进工具取得的 0.07 和 0.59 的对应值。

    Aug, 2023

  • 基于意图的语义交流的神经符号人工智能

    本研究提出了一种新的技术框架 ——NeSy AI，结合 GFlowNet 和优化问题解决方案，来学习生成 6G 系统数据，具有更高的语义可靠性，并通过验证实现了比传统通信系统更高效的、具有更好的数据推理能力的数据传输方式。

    May, 2022

  • nl2spec：使用大型语言模型将非结构化自然语言交互地翻译为时间逻辑

    通过使用大型语言模型从自然语言中推导出严格的正式说明的方法，解决了手动编写正式规范的困难，从而提出了一个框架 nl2spec。

    Mar, 2023

  • 6G 及其后的预测性切换策略：一种深度和迁移学习方法

    下一代蜂窝网络将采用机器学习进行优化，利用更高频段和更密集部署来满足各种服务需求，然而这种进化也带来了挑战，尤其是在移动性管理方面，我们提出了一种基于深度学习的算法来预测未来的服务单元，以减少切换失败和中断时间，通过转移学习优化网络目标，结果表明我们的算法可以高精度地预测未来的服务单元并大幅减少重新训练时间。

    Apr, 2024

  • POLAR-Express: 神经网络控制系统的高效而精确的正式可达性分析

    本文介绍了 POLAR-Express，一种用于验证神经网络控制系统的安全性的高效而精确的正式可达性分析工具。该工具使用泰勒模型算术来跨越神经网络层层传播泰勒模型从而计算神经网络函数的近似值，能够分析任何具有连续激活函数的前馈神经网络。文章中还提出了一种在 ReLU 激活函数上更加高效和精确传播泰勒模型的新方法。在多个数据集上的对比实验表明，POLAR-Express 在可达性分析中取得了最佳的效率和可靠性。

    Mar, 2023