FormAI Dataset

FormAI是一个新型的人工智能生成数据集，包含112,000个可编译且独立的C程序。所有程序均由GPT-3.5-turbo使用动态零样本提示技术生成，涵盖了不同复杂度的程序，从简单的字符串操作到复杂的网络管理、桌面游戏或加密任务。每个程序都根据使用基于ESBMC的正式验证方法识别的代码中的漏洞进行标记，确保无误报和误检。这些标记的样本可用于训练大型语言模型，因为它们精确地指出了软件漏洞的位置。

FormAI is a novel artificial intelligence-generated dataset comprising 112,000 compilable and independent C programs. All programs are generated by GPT-3.5-turbo using dynamic zero-shot prompting techniques, encompassing a range of complexities from simple string manipulations to intricate network management, desktop games, or cryptographic tasks. Each program is labeled based on vulnerabilities identified in the code using a formal verification method based on ESBMC, ensuring no false positives or false negatives. These labeled samples can be utilized to train large language models as they precisely indicate the locations of software vulnerabilities.

原始信息汇总

FormAI Dataset Summary

Dataset Overview

FormAI Dataset is a collection of AI-generated compilable and independent C programs with vulnerability classification. It includes two versions:

1. FormAI-v1: Contains 112,000 compilable C programs generated by GPT-3.5-turbo.
2. FormAI-v2: Recently released with 265,000 compilable C programs generated using various Large Language Models (LLMs) including Googles GEMINI-pro, OpenAIs GPT-4, TIIs 180 billion-parameter Falcon, CodeLLama2, and other compact models.

Dataset Features

• Generation Technique: Utilizes dynamic zero-shot prompting.
• Program Complexity: Varies from simple tasks like string manipulation to complex tasks such as network management, table games, or encryption.
• Vulnerability Labelling: Each program is labelled based on vulnerabilities using a formal verification method based on the Efficient SMT-based Bounded Model Checker (ESBMC).
• Use Cases: Suitable for machine learning training, testing vulnerability detection software, and other tasks requiring a substantial collection of C files.

Dataset Structure

FormAI-v1

• File Format: CSV.
• Compilation: 109,757 samples can be compiled using gcc -lm, while the remaining 3% require additional dependencies.

FormAI-v2

• File Format: JSON.
• Additional Metrics: Includes cyclomatic complexity for understanding code complexities.
• Dataset Files:
  • FormAI-v2-DATASET.7z: Contains all 265,000 C files.
  • FormAI-v2-classification.7z.001 and FormAI-v2-classification.7z.002: Contain FormAI-v2.json with vulnerability classification and C code.

Citation Information

FormAI-v1

• Paper: Presented at the 19th International Conference on Predictive Models and Data Analytics in Software Engineering (PROMISE 2023).
• Citation: https://dl.acm.org/doi/10.1145/3617555.3617874

FormAI-v2

• Paper: Recently released.
• Citation: https://arxiv.org/abs/2404.18353

Usage Guidelines

FormAI-v2

• Installation: Requires Ubuntu LTS version 22.04.03, Linux kernel version 5.19.0, and gcc 11.4.0.
• Compilation Verification: Can be tested by compiling a subset of files.
• ESBMC Usage: Used for verifying vulnerabilities; a pre-compiled binary is available.

FormAI-v1

• Installation: Similar to FormAI-v2 but with different dataset file names and versions of ESBMC.

Disclaimer

• Security Warning: Some compiled codes may have capabilities to connect to the web, scan local networks, or delete files. Users are advised to check source code before running.

搜集汇总

数据集介绍

构建方式

FormAI数据集通过动态零样本提示技术生成，利用多种大型语言模型（如GPT-4、GEMINI-pro、Falcon等）生成了大量可编译的C语言程序。这些程序涵盖了从简单字符串操作到复杂网络管理、加密等任务的不同复杂度。每个程序通过基于高效SMT的有界模型检查器（ESBMC）进行形式化验证，标记出代码中的漏洞位置，并提供了具体的反例以减少误报和漏报。此外，数据集还使用Nicad工具去除了重复的代码克隆，但仍保留了这些克隆的原始C文件，以便在模糊测试或编译器工具漏洞检测中使用。

特点

FormAI数据集包含了大量由AI生成的C语言程序，每个程序都经过形式化验证并标记了漏洞位置。数据集分为两个版本：FormAI-v1包含11.2万个程序，FormAI-v2则扩展至33.1万个程序，涵盖了更多模型生成的代码。数据集中的程序不仅可编译，还包含了代码的复杂度指标（如圈复杂度），便于机器学习分类任务。此外，数据集提供了详细的漏洞分类信息，包括漏洞的具体位置和代码片段，适合用于训练大型语言模型或测试漏洞检测工具。

使用方法

使用FormAI数据集时，首先需从GitHub克隆数据集并安装必要的依赖项。数据集中的C文件可通过7z工具解压，并使用gcc进行编译。用户可以通过提供的JSON文件获取每个程序的漏洞分类信息，并使用ESBMC工具对单个文件进行漏洞验证。数据集适用于机器学习训练、漏洞检测工具测试等任务，用户可通过命令行工具快速验证文件的编译状态，并提取特定漏洞的代码片段进行进一步分析。

背景与挑战

背景概述

FormAI数据集是一个由AI生成的大规模C程序集合，专注于漏洞分类与形式化验证。该数据集由Norbert Tihanyi等研究人员于2023年12月在PROMISE 2023会议上首次发布，其核心研究问题是通过生成式AI技术创建可编译的C程序，并利用形式化验证方法（如ESBMC）对这些程序进行漏洞分类。FormAI数据集不仅为软件安全领域提供了丰富的实验数据，还为训练大型语言模型（LLMs）提供了精确的漏洞位置信息，推动了AI在软件漏洞检测中的应用。FormAI-v2版本进一步扩展了数据规模，涵盖了331,000个C程序，并引入了多种LLM生成模型，如GPT-4、Gemini Pro等，显著提升了数据集的多样性和复杂性。

当前挑战

FormAI数据集在构建与应用过程中面临多重挑战。首先，生成式AI生成的C程序虽然可编译，但其复杂性和多样性可能导致形式化验证工具（如ESBMC）在处理时出现性能瓶颈，尤其是在处理大规模数据集时。其次，尽管数据集通过动态零样本提示技术生成程序，但仍需确保生成的程序具有足够的多样性和代表性，以避免训练模型时的偏差问题。此外，数据集中包含的克隆程序（如Type 1、Type 2等）虽然被移除，但其原始文件仍被保留，这为研究者在漏洞检测和模糊测试中提供了额外的挑战与机会。最后，数据集的编译依赖复杂的外部库和工具链，这在实际应用中可能引发兼容性问题，尤其是在不同版本的编译器和操作系统环境下。

常用场景

经典使用场景

FormAI数据集在软件安全领域具有广泛的应用，尤其是在漏洞检测和形式化验证方面。该数据集通过生成大量可编译的C程序，并结合形式化验证工具ESBMC，能够精确标注代码中的漏洞位置。研究人员可以利用这些标注数据训练机器学习模型，特别是针对大型语言模型（LLMs）的漏洞检测能力进行优化。此外，数据集中的程序涵盖了从简单字符串操作到复杂网络管理和加密任务的多层次复杂度，为研究不同复杂度代码的漏洞模式提供了丰富的实验材料。

解决学术问题

FormAI数据集解决了软件安全研究中的多个关键问题。首先，它通过形式化验证方法减少了漏洞检测中的假阳性和假阴性问题，提供了具体的反例来验证漏洞的存在。其次，数据集中的程序由多种大型语言模型生成，涵盖了广泛的代码风格和复杂度，为研究AI生成代码的漏洞模式提供了独特的数据支持。此外，数据集还通过去除克隆代码，确保了数据的多样性和代表性，为研究代码克隆与漏洞之间的关系提供了基础。

衍生相关工作

FormAI数据集衍生了许多相关研究，特别是在AI生成代码的漏洞检测和形式化验证领域。基于该数据集的研究工作主要集中在如何利用形式化验证工具（如ESBMC）提高漏洞检测的准确性，以及如何通过机器学习模型优化漏洞分类。此外，数据集还推动了代码克隆与漏洞关系的研究，特别是在克隆代码中引入新漏洞的机制方面。这些研究不仅提升了软件安全领域的理论水平，还为实际漏洞检测工具的开发提供了重要参考。