FormAI Dataset

该数据集是一个包含了112,000个人工智能生成的、可编译的且独立的C程序的大型集合，这些程序根据其存在的漏洞进行了分类。每个程序都标注了漏洞类型、行号以及存在漏洞的函数名称。此外，该数据集还提供了生成程序的详细方法，并使用高效的基于SMT的边界模型检查器（ESBMC）来识别漏洞，同时将漏洞与常见弱点枚举（CWE）编号相关联。该数据集的规模达到112,000个程序，其任务是进行C程序中的漏洞检测。This dataset comprises a large corpus of 112,000 AI-generated, compilable, standalone C programs, categorized according to the vulnerabilities present within each program. Each individual program is annotated with its specific vulnerability type, the line numbers corresponding to the vulnerability, and the name of the function hosting the vulnerability. Furthermore, detailed procedures for generating these programs are provided, and the efficient SMT-based bounded model checker (ESBMC) is employed to identify vulnerabilities, with each vulnerability linked to its corresponding Common Weakness Enumeration (CWE) identifier. Boasting a total of 112,000 programs, this dataset is tailored for the task of vulnerability detection in C programs.

搜集汇总

数据集介绍

构建方式

FormAI数据集的构建始于一种动态零样本提示技术，旨在引导大型语言模型（特别是GPT-3.5-turbo）生成多样化的C语言程序。该技术将提示词分为动态与静态两部分：动态部分从200种主题类型和100种编码风格中随机组合，形成多达20,000种独特指令，辅以温度参数调节随机性，从而确保程序在复杂度与任务类型上的广泛覆盖，涵盖从网络管理、加密算法到简单字符串处理等场景。生成的代码经由GNU C编译器筛选，仅保留可编译的程序，最终汇聚成包含112,000个独立样本的集合。随后，利用高效SMT约束的有界模型检查器ESBMC对每个样本进行形式化验证，通过符号执行与模型检测技术，在预设边界内精确识别漏洞，并输出包括漏洞类型、所在行号及函数名称在内的细粒度标签。

特点

该数据集的核心特点在于其独特的形式化验证标签体系，彻底消除了传统静态分析中常见的误报问题。ESBMC基于数学证明提供反例模型，确保每个被标记的漏洞均为确定性存在，而非概率性推测。数据集覆盖54%以上的漏洞样本，累计检测出197,800个脆弱函数，涉及算术溢出、缓冲区溢出、数组越界、空指针解引用等9大类安全缺陷，并与42个CWE标识符建立映射关系。与现有数据集不同，FormAI中的每个程序可能包含多种漏洞类型，且标签粒度细化至函数级别，为深度学习模型提供了更丰富的语义学习素材。此外，所有程序均为独立可编译的完整代码，平均长度79行，包含全部32个C语言关键字，其语法结构与真实世界项目高度相似。

使用方法

FormAI数据集适用于多种研究场景，尤其在漏洞检测工具的基准测试与机器学习模型的训练中展现独特价值。研究者可直接使用提供的.csv标签文件，其中包含文件名、漏洞类型、函数名、行号及错误类别，快速构建分类或回归任务。对于深度学习应用，数据集可被用于训练大型语言模型以学习安全编码模式，或作为微调预训练模型的负样本集合。此外，由于每个程序均能独立编译，用户可通过调整ESBMC的验证参数（如循环展开次数与超时时间）复现或扩展漏洞检测结果。该数据集还可用于模糊测试，已成功揭示ESBMC、CBMC及Clang编译器中的多个潜在缺陷。

背景与挑战

背景概述

随着大语言模型在代码生成领域的广泛采用，人工智能生成的代码是否具备足够的安全性已成为软件工程中亟待解决的核心议题。FormAI数据集由Norbert Tihanyi等人于2023年创建，隶属于阿布扎比技术创新研究院与奥斯陆大学等机构，旨在系统性地探究生成式AI在软件安全中的表现。该数据集首次大规模发布了112,000个由GPT-3.5-turbo生成的、可编译且独立的C语言程序，并利用高效的SMT约束求解模型检查器ESBMC进行形式化验证，为每个程序标注了漏洞类型、所在行号及函数名称。这一开创性工作填补了针对AI生成代码安全性进行大规模、形式化验证的数据空白，为后续的漏洞检测工具基准测试与机器学习模型训练提供了坚实的数据基础。

当前挑战

FormAI数据集所解决的领域核心挑战在于，LLM生成的C代码中普遍存在安全与正确性问题，且传统静态分析工具难以在无误报前提下准确识别这些漏洞。具体而言，数据集构建过程中面临两大挑战：其一，如何生成兼具多样性与复杂性的可编译代码，研究者通过设计包含200种主题与100种编码风格的动态零样本提示策略，组合出20,000种不同的提示模板，辅以温度参数调控，有效避免了单一模式的输出；其二，如何在大规模数据上实现无假阳性的漏洞标注，研究者依赖ESBMC的形式化验证能力，通过设置30秒超时与循环展开深度为1的边界条件，在可接受的计算资源下完成了106,139个程序的验证，并成功识别出197,800个漏洞实例，确保了标注的数学严谨性。

常用场景

经典使用场景

FormAI数据集作为首个大规模、全自动生成且经过形式化验证的C语言程序集合，在软件安全领域开辟了独特的应用范式。其经典使用场景在于评估和基准测试各类静态与动态分析工具的有效性，尤其是针对由大语言模型生成的代码中潜藏的漏洞。研究者可借助该数据集系统性地检验不同漏洞检测引擎（如Clang静态分析器、传统符号执行工具）在识别整数溢出、缓冲区溢出、空指针解引用等典型缺陷时的召回率与精准度，从而推动软件安全分析技术的演进。

衍生相关工作

FormAI数据集催生了一系列前沿探索工作，其中最引人注目的是将大语言模型与形式化验证相结合的自我修复代码范式。受该数据集启发，研究者提出了利用ESBMC输出的反例引导GPT-3.5自动修复漏洞的框架，实验表明该方法能高效修正特定类型的缺陷。此外，该数据集还推动了针对大语言模型代码生成中“模型崩溃”现象的研究，通过分析AI生成代码中漏洞模式的递归传播，为构建更鲁棒的训练数据筛选策略提供了理论依据。

数据集最近研究

最新研究方向

在人工智能与软件安全交叉领域，FormAI数据集的问世为理解大语言模型生成代码的安全性提供了前所未有的实证基础。该数据集通过动态零样本提示技术驱动GPT-3.5-turbo生成了112,000个可编译的C语言程序，并借助形式化验证工具ESBMC进行精确漏洞标注，彻底消除了误报问题。当前前沿研究方向聚焦于利用该数据集训练机器学习模型以自动检测和修复AI生成代码中的安全缺陷，同时探索大语言模型在代码生成中系统性引入漏洞的深层模式，特别是与CWE标准关联的常见脆弱性类型。这一研究热潮与生成式AI在软件开发中的爆炸式应用紧密相关，FormAI数据集不仅为基准测试提供了黄金标准，更推动了形式化方法与深度学习在软件安全领域的深度融合，对构建可信赖的AI编码助手具有里程碑意义。

相关研究论文

• The FormAI Dataset: Generative AI in Software Security Through the Lens of Formal Verification

  Technology Innovation Institute Abu Dhabi UAE · 2024年