Broken by Default: A Formal Verification Study of Security Vulnerabilities in AI-Generated Code

该研究通过 Z3 求解器对 3,500 个 AI 生成的代码工件进行形式化验证，发现所有前沿大模型生成的代码中平均有 55.8% 存在经数学证明的安全漏洞，且现有行业工具几乎无法检测出这些漏洞。

要点

这篇论文就像是一份**"AI 代码体检报告”**，而且是一份非常严厉、甚至有点令人震惊的体检报告。

简单来说，研究人员发现：现在的 AI 编程助手（比如 GitHub Copilot、ChatGPT 写代码等），在生成代码时，默认状态下就像是一个“天生带病”的工匠。如果你不特意去检查，它们写出来的代码里，超过一半都藏着严重的“安全漏洞”。

为了让你更容易理解，我们可以用几个生动的比喻来拆解这篇论文的核心内容：

1. 核心发现：AI 是“带病上岗”的

想象一下，你请了 7 位世界顶级的“数字工匠”（也就是 7 个最先进的大语言模型）来帮你盖房子（写代码）。

• 结果很糟糕：研究人员让这 7 位工匠各盖了 500 间房子（生成了 3500 段代码）。结果发现，平均有 55.8% 的房子是“危房”。
• 谁最糟糕？：GPT-4o 表现最差，62.4% 的房子都有问题，得了个"F"（不及格）。
• 谁最好？：Gemini 2.5 Flash 表现相对最好，但也只有 48.4% 的安全率，勉强得了个"D"（及格边缘）。
• 结论：没有一位工匠能拿到"C"或更好的成绩。这意味着，如果你直接让 AI 写代码而不加人工审查，你得到的代码大概率是有漏洞的。

2. 漏洞在哪里？——“算错账”的致命伤

这些漏洞主要集中在两个地方，就像盖房子时算错了材料：

• 内存分配（Memory Allocation）：比如你要买 10 块砖，AI 算错了，买了 1000 块，结果把仓库撑爆了（缓冲区溢出）。
• 整数计算（Integer Arithmetic）：这是最严重的，87% 的漏洞都出在这里。就像 AI 在计算“需要多少钢筋”时，数字太大算错了，导致整个结构瞬间崩塌。

比喻：这就好比 AI 在写代码时，总是习惯性地忽略“如果数字太大怎么办”这个问题。就像它默认“永远不会有人买 10 亿块砖”，但一旦真的有人买了，房子就塌了。

3. 研究方法：用“数学证明”代替“猜谜”

以前的研究就像是在找“通缉犯”，拿着照片（特征库）去比对，觉得“长得像”就是坏人。

• 这篇论文做了什么？ 他们请了一位**“数学侦探”**（Z3 SMT 求解器）。
• 怎么做的？ 这个侦探不靠猜，而是用纯数学逻辑去证明：“看，只要输入这个数字，你的代码一定会崩溃。”
• 结果：他们找到了 1055 个**“铁证如山”**的漏洞。而且，他们真的在电脑上运行了这些代码，看着它们像炸弹一样爆炸（内存溢出、数据泄露），证实了这些漏洞是真实存在的，不是吓唬人的。

4. 两个令人震惊的“实验”

实验一：给 AI 戴个“紧箍咒”有用吗？（安全指令）

研究人员试着在提示词里加了一句：“请写出最安全的代码，注意不要溢出！”

• 结果：就像给一个习惯乱跑的孩子戴了个帽子，效果微乎其微。
• 关键细节：这个“紧箍咒”实验是在一个较小的子集（50 个提示词，v1 版本）上进行的。在这个子集中，漏洞率仅从 64.8% 降到了 60.8%（下降了约 4 个百分点）。
• 比喻：这就像告诉一个习惯闯红灯的司机“请小心驾驶”，但他还是会在 60% 的时候闯红灯。这说明AI 的“坏习惯”是刻在骨子里的（训练数据的问题），光靠口头提醒没用。（注：虽然实验规模较小，但趋势表明单纯依靠提示词优化难以解决根本问题）。

实验二：AI 能自己发现错误吗？（生成 vs 审查）

研究人员让 AI 先写代码，然后再让它自己当“考官”去检查刚才写的代码。

• 结果：
  • 写代码时：它 55.8% 的时候写错。
  • 当考官时：它 78.7% 的时候能认出错误。
• 比喻：这就像是一个**“双标”的厨师**。他做饭时总是把盐放多（生成漏洞），但如果你把菜端给他让他尝，他能立刻尝出来“太咸了”（识别漏洞）。
• 结论：AI 不是不懂安全知识，而是它在主动创作时，根本想不起来去用这些知识。

5. 现有的工具能救场吗？（静态分析工具）

大家可能会想：“没关系，我们有专业的代码扫描工具（像 Semgrep, CodeQL 等）来检查啊。”

• 结果：这些工具几乎全废了。
• 数据：对于 AI 生成的那些“铁证如山”的数学漏洞，现有的 6 种顶级工具加起来，只抓出了 7.6%。剩下的 97.8% 的漏洞，它们完全看不见。
• 比喻：现有的工具就像是用“金属探测器”去找“塑料炸弹”。AI 生成的漏洞是那种“数学逻辑上的塑料炸弹”，探测器扫过去完全没反应。只有那个“数学侦探”（Z3）能发现。

6. 给普通人的建议（总结）

这篇论文给所有使用 AI 写代码的人敲响了警钟：

1. 不要盲目信任：把 AI 生成的代码当成“未经验证的原材料”，绝对不能直接用在银行、医疗或安全系统里。
2. 别指望提示词：在提示词里加“要安全”这种话，作用很小（基于小规模实验的显著性趋势）。
3. 别只靠旧工具：传统的代码扫描工具抓不住 AI 特有的这种“数学逻辑漏洞”。
4. 必须人工介入：对于关键代码，必须有人类专家进行严格审查，或者使用更高级的数学验证方法。

一句话总结：
目前的 AI 编程助手就像是一个才华横溢但粗心大意的天才，它写代码很快，但默认状态下一半以上都有致命的安全漏洞。而且，现有的检查工具大多抓不住这些漏洞，人类必须亲自把关，否则后果不堪设想。

技术摘要

论文技术总结：《Broken by Default：AI 生成代码中安全漏洞的形式化验证研究》

1. 研究背景与问题定义

随着 AI 编程助手（如 GitHub Copilot、ChatGPT 等）在安全敏感领域（如 Web 后端、嵌入式系统、加密库）的广泛应用，其生成代码的安全性已成为关键隐患。

• 核心问题：现有的评估方法主要依赖静态模式匹配或人工审查，无法确证（Definitively Establish）漏洞的可利用性（Exploitability）。
• 研究缺口：缺乏对 AI 生成代码中漏洞是否真正可被利用的数学证明，且现有工具对深层逻辑漏洞（如整数溢出导致的内存分配错误）的检测能力存疑。
• 研究目标：通过形式化验证方法，量化七大前沿大语言模型（LLM）在生成安全敏感代码时的漏洞率，并验证这些漏洞是否具备实际的可利用性。

2. 方法论 (Methodology)

2.1 基准测试设计

• 数据集：构建了包含 500 个提示词（Prompts）的基准测试集，涵盖 5 个 CWE 类别（每类 100 个）：
  • MEM (CWE-131/190): 内存分配、数组索引、动态内存管理。
  • INT (CWE-190/195): 整数运算、类型转换、有符号/无符号算术。
  • AUTH (CWE-916): 密码哈希、认证令牌生成。
  • CRYPTO (CWE-327/330): 密钥生成、随机数使用。
  • INP (CWE-89/22/78): SQL 构建、文件路径处理、Shell 命令。
• 模型选择：评估了 7 个前沿 LLM（截至 2026 年 Q1-Q2），包括 GPT-4o, GPT-4.1, Claude Haiku 4.5, Gemini 2.5 Flash, Mistral Large, Llama 3.3 70B, Llama 4 Scout。
• 配置：所有模型均在温度（Temperature）为 0 的确定性模式下通过生产 API 查询，确保结果可复现。

2.2 COBALT 分析管道

研究团队开发了 COBALT 分析引擎，结合静态分析与形式化验证：

1. CWE 模式提取：利用正则和 AST 模式识别潜在漏洞点。
2. Z3 SMT 编码：将漏洞条件编码为 Z3 可满足性模理论（SMT）公式。
   • 示例：对于整数溢出，将变量 $n$ 定义为 32 位位向量，检查 $n \times \text{sizeof}(T) < n$ 是否可满足。
3. 见证提取 (Witness Extraction)：若 Z3 返回 SAT（可满足），则提取具体的输入值（如 $n = 2^{30} + 1$）作为可被利用的输入证据。
   • Z3 SAT：形式化证明可利用。
   • PATTERN MATCH：结构上存在漏洞，但未通过 Z3 验证。
   • CLEAN：未检测到漏洞。

2.3 运行时验证

• 选取 7 个代表性漏洞构建概念验证（PoC）代码。
• 使用 GCC AddressSanitizer (ASAN) 编译并运行，输入 Z3 提取的具体见证值，确认是否触发运行时崩溃（如堆缓冲区溢出）。

2.4 辅助实验

1. 安全提示消融实验：在系统提示中显式加入安全指令，观察漏洞率变化。注：此消融实验仅在包含 50 个提示词的子集（v1）上进行，而非完整的 500 个提示词基准测试集，以确保实验的可复现性与资源可控性。
2. 静态工具对比：将 COBALT 结果与 6 种行业标准工具（Semgrep, Bandit, Cppcheck, Clang SA, FlawFinder, CodeQL）进行对比。
3. 生成 - 审查不对称性实验：让模型审查其自身生成的漏洞代码，测试其识别能力。

3. 关键贡献 (Key Contributions)

1. 形式化验证的引入：首次大规模使用 Z3 SMT 求解器 对 AI 生成代码进行形式化验证，提供了数学上确凿的漏洞可利用性证明（Ground-Truth），而非基于启发式的推测。
2. 大规模基准测试：评估了 7 个模型生成的 3,500 个代码工件，覆盖了 5 个关键安全类别。
3. 工具检测能力的结构性差距：揭示了现有工业级静态分析工具在检测 AI 生成的整数溢出类漏洞时存在结构性盲区（97.8% 的 Z3 证明漏洞未被检测）。
4. 生成 - 审查不对称性发现：证明了模型具备识别自身漏洞的知识（审查模式下识别率 78.7%），但在生成模式下却频繁失败，表明问题在于知识的应用而非知识本身的缺失。

4. 主要结果 (Key Results)

4.1 总体漏洞率

• 平均漏洞率：所有模型生成的代码中，55.8% 至少包含一个 COBALT 识别的漏洞。
• 形式化证明：在 3,500 个工件中，有 1,055 个漏洞被 Z3 形式化证明为可利用（Z3 SAT）。
• 模型表现：
  • 最差：GPT-4o (62.4%, 等级 F)。
  • 最好：Gemini 2.5 Flash (48.4%, 等级 D)。
  • 结论：没有任何一个模型达到 C 级或更好，所有模型默认生成的代码在安全上都是“损坏的”（Broken by Default）。

4.2 漏洞分布

• 最高发类别：整数运算 (INT) 漏洞率高达 87%，其次是内存分配 (MEM) 为 67%。
• 典型模式：所有模型在 malloc(n * sizeof(T)) 中普遍缺乏溢出检查，导致整数溢出进而引发堆缓冲区溢出。

4.3 运行时验证

• 在 7 个选定的 PoC 测试中，6 个 成功触发了 ASAN 报告的运行时错误（如堆缓冲区溢出、OOB 读取）。
• 密码哈希漏洞（CWE-916）被证实可在 0.01ms 内被破解。

4.4 辅助实验发现

1. 安全指令无效：在提示词中加入“编写安全代码”等显式指令，在 50 个提示词的子集（v1） 上仅将平均漏洞率从 64.8% 降低至 60.8%（下降 4 个百分点），且 4/5 的模型仍为 F 级。
2. 工具检测差距：
   • 6 种行业工具联合仅检测到 7.6% 的工件漏洞。
   • 对于 90 个经 Z3 形式化证明的漏洞，工具检测率为 0%（CodeQL 等工具完全漏报），漏报率高达 97.8%。
   • 原因：现有工具基于模式匹配或数据流分析，无法进行跨域整数算术推理（如证明 $n \times \text{size}$ 会溢出）。
3. 生成 - 审查不对称：模型在审查模式下能正确识别 78.7% 的自身漏洞，但在生成模式下却以 55.8% 的概率生成这些漏洞。

5. 研究意义与结论

5.1 核心结论

• AI 代码默认不安全：当前 LLM 生成的代码在安全敏感领域存在极高的漏洞风险，且这种风险是系统性的，无法通过简单的提示词工程（Prompt Engineering）解决。
• 现有工具失效：传统的静态分析工具（包括 CodeQL）无法检测 AI 生成代码中常见的整数溢出导致的内存分配错误，因为它们缺乏形式化的算术推理能力。
• 形式化验证的必要性：Z3 SMT 求解器是建立 AI 生成代码漏洞“真实可利用性”（Ground-Truth Exploitability）的唯一有效方法。

5.2 对开发者的建议

1. 将 AI 生成的 C/C++ 代码视为未经审查的代码，必须进行显式的安全审计。
2. 对所有 AI 生成的系统代码启用 -fsanitize=address,undefined 进行运行时检测。
3. 不要依赖“编写安全代码”的提示词前缀作为缓解措施。
4. 不要依赖 Semgrep、CodeQL 等工具单独检测 AI 生成的整数溢出漏洞。
5. 对于内存分配算术，必须使用形式化验证或严格的人工审查。

5.3 未来展望

该研究强调了在 AI 代码审查流水线中集成形式化验证（如 Z3）的紧迫性，特别是针对内存安全和算术逻辑密集型任务。未来的工作将扩展到更多编程语言（Go, Rust, JS）以及针对特定 CWE 类别的微调效果评估。

---

论文元数据：

• 标题: Broken by Default: A Formal Verification Study of Security Vulnerabilities in AI-Generated Code
• 作者: Dominik Blain, Maxime Noiseux (Cobalt AI)
• 日期: 2026 年 4 月 5 日
• 数据集: 3,500 个代码工件，7 个模型，500 个提示词。
• 开源地址: https://github.com/dom-omg/broken-by-default