This study provides a comparative analysis of state-of-the-art large language
models (LLMs), analyzing how likely they generate vulnerabilities when writing
simple C programs using a neutral zero-shot prompt. We address a significant
gap in the literature concerning the security properties of code produced by
these models without specific directives. N. Tihanyi et al. introduced the
FormAI dataset at PROMISE '23, containing 112,000 GPT-3.5-generated C programs,
with over 51.24% identified as vulnerable. We expand that work by introducing
the FormAI-v2 dataset comprising 265,000 compilable C programs generated using
various LLMs, including robust models such as Google's GEMINI-pro, OpenAI's
GPT-4, and TII's 180 billion-parameter Falcon, to Meta's specialized 13
billion-parameter CodeLLama2 and various other compact models. Each program in
the dataset is labelled based on the vulnerabilities detected in its source
code through formal verification using the Efficient SMT-based Context-Bounded
Model Checker (ESBMC). This technique eliminates false positives by delivering
a counterexample and ensures the exclusion of false negatives by completing the
verification process. Our study reveals that at least 63.47% of the generated
programs are vulnerable. The differences between the models are minor, as they
all display 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 risk assessment and
validation.

本研究比较分析了最先进的大型语言模型（LLMs），研究了它们使用中性的零 - shot 提示来编写简单 C 程序时生成漏洞的可能性。通过引入 FormAI-v2 数据集，该研究扩展了之前的工作，并包含了使用各种 LLMs 生成的 265,000 个可编译的 C 程序。研究揭示了至少 63.47％的生成程序存在漏洞，并提醒在生产环境中使用 LLMs 生成的代码时需要进行风险评估和验证。

中性提示是否会产生不安全的代码？FormAI-v2 数据集：标记大型语言模型生成的代码中的漏洞

Do Neutral Prompts Produce Insecure Code? FormAI-v2 Dataset: Labelling  Vulnerabilities in Code Generated by Large Language Models

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.

FormAI 数据集利用动态零 - shot 提示技术构建，包含 11.2 万个 AI 生成的可以编译和独立运行的 C 程序，按漏洞类型进行了分类，并采用 SMT-based Bounded Model Checker 方法进行了验证，检测出漏洞并提供反例，用于评估各种静态和动态分析工具的效果以及用于训练大型语言模型和机器学习算法。