FormAI 数据集：通过形式化验证视角审视生成式 AI 在软件安全中的应用

本文提出 FormAI 数据集，这是一个包含 112,000 个由 AI 生成的、可编译且相互独立的 C 程序及其漏洞分类的大型集合。我们引入了一种动态零样本提示技术，用于利用大语言模型（LLMs）生成多样化的程序。该数据集由 GPT-3.5-turbo 生成，包含复杂度各异的程序：部分程序处理网络管理、棋类游戏或加密等复杂任务，另一些则处理字符串操作等较简单任务。每个程序都标注了源代码中发现的漏洞，指明其类型、行号及存在漏洞的函数名。这是通过采用基于高效 SMT 的有界模型检查器（ESBMC）的形式化验证方法实现的，该方法运用模型检查、抽象解释、约束编程和可满足性模理论来推理程序的安全/安全属性。此方法可明确检测漏洞，并提供称为反例的形式化模型，从而杜绝产生误报的可能性。我们已将识别出的漏洞与通用缺陷枚举（CWE）编号相关联。我们公开了这 112,000 个程序的源代码，并附带一个单独文件记录每个程序中检测到的漏洞，使该数据集非常适于训练 LLM 和机器学习算法。我们的研究表明，根据 ESBMC 的检测，GPT-3.5 生成的程序中有 51.24% 含有漏洞，从而对软件安全性与安全保障构成显著风险。