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

Norbert Tihanyi, Tamas Bisztray, Ridhi Jain, Mohamed Amine Ferrag, Lucas C. Cordeiro, Vasileios Mavroeidis

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

31 Downloads (Pure)

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 a diverse set of 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 such as 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 performs 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. This property of the dataset makes it suitable for evaluating the effectiveness of various static and dynamic analysis tools. Furthermore, we have associated the identified vulnerabilities with relevant Common Weakness Enumeration (CWE) numbers. We make the source code available for the 112,000 programs, accompanied by a comprehensive list detailing the vulnerabilities detected in each individual program including location and function name, which makes the dataset ideal to train LLMs and machine learning algorithms.
Original languageEnglish
Title of host publicationPROMISE '23
Subtitle of host publicationThe 19th International Conference on Predictive Models and Data Analytics in Software Engineering
Publication statusAccepted/In press - 29 Jul 2023

Keywords

  • cs.DB
  • cs.AI

Fingerprint

Dive into the research topics of 'The FormAI Dataset: Generative AI in Software Security Through the Lens of Formal Verification'. Together they form a unique fingerprint.

Cite this