This paper introduces Auto-modeling of Formal Verification with Real-world Prompting for 5G and NextG protocols (AVRE), a novel system designed for the formal verification of Next Generation (NextG) communication protocols, addressing the increasing complexity and scalability challenges in network protocol design and verification. Utilizing Large Language Models (LLMs), AVRE transforms protocol descriptions into dependency graphs and formal models, efficiently resolving ambiguities and capturing design intent. The system integrates a transformer model with LLMs to autonomously establish quantifiable dependency relationships through cross- and self-attention mechanisms. Enhanced by iterative feedback from the HyFuzz experimental platform, AVRE significantly advances the accuracy and relevance of formal verification in complex communication protocols, offering a groundbreaking approach to validating sophisticated communication systems. We compare CAL's performance with state-of-the-art LLM-based models and traditional time sequence models, demonstrating its superiority in accuracy and robustness, achieving an accuracy of 95.94\% and an AUC of 0.98. This NLP-based approach enables, for the first time, the creation of exploits directly from design documents, making remarkable progress in scalable system verification and validation.

翻译：本文介绍了面向5G与NextG协议形式化验证的自动建模系统AVRE（基于真实场景提示），该系统专为下一代（NextG）通信协议的形式化验证而设计，旨在应对网络协议设计与验证中日益增长的复杂性和可扩展性挑战。AVRE利用大语言模型（LLMs）将协议描述转化为依赖图与形式化模型，高效消除歧义并捕捉设计意图。该系统将Transformer模型与LLMs相集成，通过交叉注意力与自注意力机制自主建立可量化的依赖关系。借助HyFuzz实验平台的迭代反馈增强，AVRE显著提升了复杂通信协议形式化验证的准确性与相关性，为验证精密通信系统提供了突破性方法。我们将CAL的性能与基于LLM的最先进模型及传统时序模型进行对比，证明了其在准确性与鲁棒性上的优越性：准确率达95.94%，AUC达0.98。这种基于自然语言处理的方法首次实现了从设计文档直接生成漏洞利用代码，在可扩展系统验证与确认领域取得了显著进展。