用大模型+形式化验证自动检测加密协议漏洞
CryptoFormalEval: Integrating LLMs and Formal Verification for Automated Cryptographic Protocol Vulnerability Detection
- 构建新协议漏洞数据集，让大模型与Tamarin协作找漏洞
- 实测前沿大模型在该基准上检出率不足50%
- 为安全领域融合AI与符号推理提供可量化参考
加密协议是保障现代数字基础设施安全的基础，但常在未经形式化验证的情况下部署，可能导致系统易受攻击。而传统形式化验证方法复杂耗时，缺乏自动化。本文提出一个评估基准，测试大语言模型（LLMs）通过与Tamarin——一种协议验证定理证明器交互，自主识别新型加密协议漏洞的能力。我们构建了经人工验证的、含缺陷的新通信协议数据集，并设计方法自动验证大模型发现的漏洞。当前前沿模型在该基准上的表现揭示了将大模型与符号推理系统结合用于网络安全应用的潜力与局限。
原文摘要 · Abstract (English)
Cryptographic protocols play a fundamental role in securing modern digital infrastructure, but they are often deployed without prior formal verification. This could lead to the adoption of distributed systems vulnerable to attack vectors. Formal verification methods, on the other hand, require complex and time-consuming techniques that lack automatization. In this paper, we introduce a benchmark to assess the ability of Large Language Models (LLMs) to autonomously identify vulnerabilities in new cryptographic protocols through interaction with Tamarin: a theorem prover for protocol verification. We created a manually validated dataset of novel, flawed, communication protocols and designed a method to automatically verify the vulnerabilities found by the AI agents. Our results about the performances of the current frontier models on the benchmark provides insights about the possibility of cybersecurity applications by integrating LLMs with symbolic reasoning systems.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。