用数学验证发现大模型生成代码55.8%含漏洞，没有一个模型能达安全标准。
Broken by Default: A Formal Verification Study of Security Vulnerabilities in AI-Generated Code
- 通过Z3求解器对生成代码做形式化验证，找真实漏洞。
- 55.8%的代码有可证明漏洞，最高仅达D级安全评分。
- 多数工具漏检97.8%漏洞，模型自己也难识别生成的缺陷。
AI编程助手现被用于生成安全敏感领域的生产代码，但其输出的可利用性尚未量化。本文通过「Broken by Default」研究，对七款主流大模型在500个安全关键提示（涵盖五个CWE类别，每类100个）下生成的3,500个代码片段进行形式化验证。每个片段均经由COBALT分析流程输入Z3 SMT求解器，以获得数学可满足性证据，而非依赖模式匹配的启发式方法。结果显示，所有模型中55.8%的代码包含至少一个被COBALT识别的漏洞；其中1,055个经由Z3可满足性证据被正式证明。GPT-4o表现最差，漏洞率达62.4%（评级F）；Gemini 2.5 Flash最优，为48.4%（评级D）。无一模型达到优于D的等级。六项代表性发现经GCC AddressSanitizer运行时崩溃验证确认。三项辅助实验表明：（1）明确的安全指令仅将平均漏洞率降低4个百分点；（2）六款工业工具联合使用漏检率达97.8%；（3）模型在审查模式下可识别自身生成漏洞的80.7%，但在默认生成状态下仍以55.8%的概率输出漏洞代码。
原文摘要 · Abstract (English)
AI coding assistants are now used to generate production code in security-sensitive domains, yet the exploitability of their outputs remains unquantified. We address this gap with Broken by Default: a formal verification study of 3,500 code artifacts generated by seven widely-deployed LLMs across 500 security-critical prompts (five CWE categories, 100 prompts each). Each artifact is subjected to the Z3 SMT solver via the COBALT analysis pipeline, producing mathematical satisfiability witnesses rather than pattern-based heuristics. Across all models, 55.8% of artifacts contain at least one COBALT-identified vulnerability; of these, 1,055 are formally proven via Z3 satisfiability witnesses. GPT-4o leads at 62.4% (grade F); Gemini 2.5 Flash performs best at 48.4% (grade D). No model achieves a grade better than D. Six of seven representative findings are confirmed with runtime crashes under GCC AddressSanitizer. Three auxiliary experiments show: (1) explicit security instructions reduce the mean rate by only 4 points; (2) six industry tools combined miss 97.8% of Z3-proven findings; and (3) models identify their own vulnerable outputs 78.7% of the time in review mode yet generate them at 55.8% by default.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。