默认即破损：AI生成代码安全漏洞的形式化验证研究
密码学与安全
2026-04-09 v2 人工智能
软件工程
摘要
AI编程助手现在被用于在安全敏感领域生成生产代码，但其输出的可利用性仍未被量化。我们通过Broken by Default填补了这一空白：对七个广泛部署的LLM生成的3500个代码片段进行形式化验证研究，涉及500个安全关键提示（五个CWE类别，每个100个提示）。每个代码片段通过COBALT分析流水线提交给Z3 SMT求解器，产生数学可满足性见证而非基于模式的启发式方法。在所有模型中，55.8%的代码片段包含至少一个COBALT识别的漏洞；其中1055个通过Z3可满足性见证被形式化证明。GPT-4o以62.4%领先（等级F）；Gemini 2.5 Flash表现最佳，为48.4%（等级D）。没有模型达到优于D的等级。七项代表性发现中的六项通过GCC AddressSanitizer的运行时崩溃得到确认。三项辅助实验表明：(1) 显式安全指令仅将平均率降低4个百分点；(2) 六种行业工具combined遗漏了97.8%的Z3证明发现；(3) 模型在审查模式下78.7%的时间识别出自己的脆弱输出，但默认情况下仍以55.8%的比例生成它们。
引用
@article{arxiv.2604.05292,
title = {Broken by Default: A Formal Verification Study of Security Vulnerabilities in AI-Generated Code},
author = {Dominik Blain and Maxime Noiseux},
journal= {arXiv preprint arXiv:2604.05292},
year = {2026}
}
备注
8 pages, 6 tables, empirical study