How secure is AI-generated Code: A Large-Scale Comparison of Large Language Models

📄 arXiv: 2404.18353v2 📥 PDF

作者: Norbert Tihanyi, Tamas Bisztray, Mohamed Amine Ferrag, Ridhi Jain, Lucas C. Cordeiro

分类: cs.CR, cs.AI, cs.PL

发布日期: 2024-04-29 (更新: 2024-12-11)

备注: Accepted and will be shortly published at Empirical Software Engineering (EMSE). Journal Impact Factor: 3.5 (2023)

DOI: 10.1007/s10664-024-10590-1.

💡 一句话要点

比较大型语言模型生成代码的安全性，揭示潜在漏洞

🎯 匹配领域: 支柱九：具身大模型 (Embodied Foundation Models)

关键词: 大型语言模型 代码生成 安全漏洞 正式验证 C程序 风险评估 模型检查

📋 核心要点

  1. 现有大型语言模型在生成代码时容易引入安全漏洞，缺乏有效的评估机制。
  2. 本研究通过引入FormAI和FormAI-v2数据集，系统性地评估多种LLMs生成C程序的安全性。
  3. 实验结果显示，生成程序中至少62.07%存在漏洞，模型间的差异微小，提示需谨慎使用生成代码。

📝 摘要（中文）

本研究比较了多种先进的大型语言模型（LLMs）在使用中立的零-shot提示生成C程序时，产生漏洞的倾向。研究中引入了FormAI数据集，包含由GPT-3.5-turbo生成的112,000个C程序，其中超过51.24%被识别为存在漏洞。我们扩展了这一研究，涉及9种最先进的模型，并引入了FormAI-v2数据集，包含331,000个可编译的C程序。每个程序都通过高效的SMT基础上下文有界模型检查器（ESBMC）进行正式验证，以检测源代码中的漏洞。研究结果显示，至少62.07%的生成程序存在漏洞，模型间的差异较小，表明在生产环境中使用LLMs生成的代码需要适当的风险评估和验证。

🔬 方法详解

问题定义：本研究旨在解决大型语言模型在生成C程序时可能引入的安全漏洞问题。现有方法缺乏对生成代码安全性的系统评估，导致潜在风险未被充分识别。

核心思路：通过构建FormAI和FormAI-v2数据集，利用正式验证技术对生成的C程序进行漏洞检测，提供更为可靠的安全评估。

技术框架：研究采用了高效的SMT基础上下文有界模型检查器（ESBMC），对生成的C程序进行全面的漏洞检测，确保检测的准确性和全面性。

关键创新：引入了大规模的FormAI-v2数据集，包含331,000个可编译的C程序，并通过正式验证技术显著提高了漏洞检测的准确性，减少了假阳性和假阴性。

关键设计：在漏洞检测过程中，使用了高效的模型检查算法，确保每个程序的漏洞都能被准确识别，并提供具体的反例以支持验证过程。通过这种方式，研究有效提升了对生成代码安全性的评估能力。

🖼️ 关键图片

fig_0
fig_1
fig_2

📊 实验亮点

实验结果显示，至少62.07%的生成程序存在漏洞，表明大型语言模型在代码生成中的安全性问题不容忽视。尽管不同模型间的漏洞生成差异较小，但整体结果强调了在生产环境中使用生成代码的风险。

🎯 应用场景

该研究的潜在应用领域包括软件开发、代码审计和安全评估等。随着AI在编程中的应用日益普及，确保生成代码的安全性将对软件质量和系统安全产生重要影响。未来，研究成果可为开发安全可靠的AI编程工具提供理论基础和实践指导。

📄 摘要（原文）

This study compares state-of-the-art Large Language Models (LLMs) on their tendency to generate vulnerabilities when writing C programs using a neutral zero-shot prompt. Tihanyi et al. introduced the FormAI dataset at PROMISE'23, featuring 112,000 C programs generated by GPT-3.5-turbo, with over 51.24% identified as vulnerable. We extended that research with a large-scale study involving 9 state-of-the-art models such as OpenAI's GPT-4o-mini, Google's Gemini Pro 1.0, TII's 180 billion-parameter Falcon, Meta's 13 billion-parameter Code Llama, and several other compact models. Additionally, we introduce the FormAI-v2 dataset, which comprises 331 000 compilable C programs generated by these LLMs. Each program in the dataset is labeled based on the vulnerabilities detected in its source code through formal verification, using the Efficient SMT-based Context-Bounded Model Checker (ESBMC). This technique minimizes false positives by providing a counterexample for the specific vulnerability and reduces false negatives by thoroughly completing the verification process. Our study reveals that at least 62.07% of the generated programs are vulnerable. The differences between the models are minor, as they all show similar coding errors with slight variations. Our research highlights that while LLMs offer promising capabilities for code generation, deploying their output in a production environment requires proper risk assessment and validation.