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

TL;DR

The paper introduces FormAI, a large-scale dataset of $112{,}000$ AI-generated, compilable C programs labeled for vulnerabilities via formal verification with ESBMC, addressing the risk of AI-generated code. It employs a dynamic zero-shot prompting strategy with GPT-3.5-turbo to create diverse, small programs that are then verified within a bounded depth to produce counterexamples and CWE mappings. The study reports a vulnerability rate of $>54\%$ among analyzed samples and provides detailed labeling (filename, line, function, vulnerability type) along with CWE associations, enabling ML-based vulnerability detection and verification benchmarking. The FormAI dataset, its CWE distribution, and the accompanying CSV labels offer a valuable resource for fuzzing, verification tool evaluation, and the development of safer AI-assisted software engineering workflows, while also highlighting areas for improvement in current formal verification tooling.

Abstract

This paper presents the FormAI dataset, a large collection of 112, 000 AI-generated compilable and independent C programs with vulnerability classification. We introduce a dynamic zero-shot prompting technique constructed to spawn diverse programs utilizing Large Language Models (LLMs). The dataset is generated by GPT-3.5-turbo and comprises programs with varying levels of complexity. Some programs handle complicated tasks like network management, table games, or encryption, while others deal with simpler tasks like string manipulation. Every program is labeled with the vulnerabilities found within the source code, indicating the type, line number, and vulnerable function name. This is accomplished by employing a formal verification method using the Efficient SMT-based Bounded Model Checker (ESBMC), which uses model checking, abstract interpretation, constraint programming, and satisfiability modulo theories to reason over safety/security properties in programs. This approach definitively detects vulnerabilities and offers a formal model known as a counterexample, thus eliminating the possibility of generating false positive reports. We have associated the identified vulnerabilities with Common Weakness Enumeration (CWE) numbers. We make the source code available for the 112, 000 programs, accompanied by a separate file containing the vulnerabilities detected in each program, making the dataset ideal for training LLMs and machine learning algorithms. Our study unveiled that according to ESBMC, 51.24% of the programs generated by GPT-3.5 contained vulnerabilities, thereby presenting considerable risks to software safety and security.

Figures (5)

• Figure 1: AI-driven dataset generation and vulnerability labeling framework. A random type and style combination is selected for each prompt, instructing the LLM module to generate a C program. The compilable programs are fed to the BMC module, which performs the classification based on formal verification techniques.
• Figure 2: Insecure code generated by gpt-3.5-turbo. The program reads two numbers, where the addition can result in a value outside of the range “int” can represent, which may lead to integer overflow.
• Figure 3: The counterexample provided for Figure 2. using ESBMC version 7.2.0. Note this is only part of the output specifically for integer overflow, which we wanted to bring forward for this example.
• Figure 4: Dynamic code generation prompt
• Figure 5: Dynamic prompt creation.