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

• URL: http://arxiv.org/abs/2604.05292v2
• Date: Wed, 08 Apr 2026 16:49:43 GMT
• Title: Broken by Default: A Formal Verification Study of Security Vulnerabilities in AI-Generated Code
• Abstract summary: Broken by Default is a formal verification study of 3,500 code artifacts generated by seven widely-deployed LLMs across 500 security-critical prompts.<n>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.<n>GPT-4o leads at 62.4% (grade F); Gemini 2.5 Flash performs best at 48.4% (grade D)
• Score: 0.0
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: 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.

Related papers

• Efficient Visual Pointing for Embodied AI:Agent-Driven Data Synthesis, Cross-Block Attention, and Iterative Correction [55.11480729304395]
  We describe our PointArena 2026 solution, which achieves 77.2% overall accuracy and ranks second on the benchmark.<n>The ap proach targets three failure modes. First, agent-driven syn thesis builds large semantic and anchor-relative candidate pools.<n>Second, a determinis tic steerable-data pipeline creates a verified 10,000-sample main set, plus reserve samples, using masks, templates, and path verification.
  arXiv  Detail & Related papers  (2026-06-29T06:39:03Z)
• Empirical Software Engineering TerraProbe: A Layered-Oracle Framework for Detecting Deceptive Fixes in LLM-Assisted Terraform [0.0]
  Security misconfigurations in Terraform Infrastructure-as-Code are a growing risk in cloud deployments.<n>Existing evaluations often treat a repair as successful when the targeted static-analysis finding disappears.<n>This paper presents TerraProbe, a five-layer oracle framework for evaluating LLM-assisted Terraform security repair.
  arXiv  Detail & Related papers  (2026-06-25T04:21:15Z)
• Context-Based Adversarial Attacks on AI Code Generators: Vulnerability Analysis and Implications [0.0]
  This research presents a systematic investigation of context-based adversarial attacks.<n> strategically crafted contextual inputs, including comments, documentation, variable names, bias large language models toward generating exploitable code.<n>Our dual-layer defense framework achieves 89.1% detection rate with 0.3% false positives and 520ms latency.
  arXiv  Detail & Related papers  (2026-06-09T14:51:59Z)
• Knowledge Index of Noah's Ark [63.143852586221534]
  We introduce KINA, an 899-item benchmark across 261 fine-grained disciplines.<n>We prove a bonus-on-bar tournament weakly FOSD-dominates flat payment in released-review quality.<n>The top model, Gemini-3.1-Pro-Preview, reaches 53.17%, followed by Claude-Opus-4.6 at 49.92% and GPT-5.4 at 48.55%.
  arXiv  Detail & Related papers  (2026-06-03T17:06:49Z)
• Minimal Prompt Perturbations Lead to Code Vulnerabilities: Prompt Fragility and Hidden-State Signals in Coding LLMs [46.747768845221735]
  We show that mutations as small as a single-character change can flip generated code from secure to vulnerable.<n>Results show that input-handling flaws can be caught before generation while secure-defaults flaws require intervention during decoding.
  arXiv  Detail & Related papers  (2026-05-28T10:30:28Z)
• Agentic Proving for Program Verification [44.663012714194025]
  Agentic systems have emerged as state-of-the-art approaches for automated theorem proving in formal mathematics.<n>We evaluate Claude Code in an agentic proving framework on CLEVER, a Lean 4 benchmark for verifiable code generation.
  arXiv  Detail & Related papers  (2026-05-22T15:41:27Z)
• MOSAIC-Bench: Measuring Compositional Vulnerability Induction in Coding Agents [2.1942030377331245]
  Coding agents often pass per-prompt safety review yet ship exploitable code when their tasks are decomposed into routine engineering tickets.<n>We introduce MOSAIC-Bench, a benchmark of 199 three-stage attack chains paired with deterministic exploit oracles on deployed software substrates.<n>We show that nine production coding agents compose innocuous tickets at 53-86% end-to-end ASR with only two refusals across all staged runs.
  arXiv  Detail & Related papers  (2026-05-05T16:38:23Z)
• SecPI: Secure Code Generation with Reasoning Models via Security Reasoning Internalization [50.71047638695205]
  Reasoning language models (RLMs) are increasingly used in programming.<n>Yet, even state-of-the-art RLMs frequently introduce critical security vulnerabilities in generated code.<n>We present SecPI, a fine-tuning pipeline that teaches RLMs to internalize structured security reasoning.
  arXiv  Detail & Related papers  (2026-04-04T04:29:11Z)
• Credential Leakage in LLM Agent Skills: A Large-Scale Empirical Study [51.717224133855886]
  Third-party skills extend LLM agents with powerful capabilities but often handle sensitive credentials in privileged environments.<n>We analyze 17,022 skills (sampled from 170,226 on SkillsMP) using static analysis, sandbox testing, and manual inspection.<n>We identify 520 vulnerable skills with 1,708 issues and derive a taxonomy of 10 leakage patterns (4 accidental and 6 adversarial)
  arXiv  Detail & Related papers  (2026-04-03T14:50:16Z)
• Emergent Formal Verification: How an Autonomous AI Ecosystem Independently Discovered SMT-Based Safety Across Six Domains [0.0]
  We propose a unified framework that applies Z3-based verification across all six output classes through a common API.<n>We evaluate it on 181 test cases across five implemented domains, achieving 100% classification accuracy with zero false positives and zero false negatives.
  arXiv  Detail & Related papers  (2026-03-22T10:02:16Z)
• Safety Recovery in Reasoning Models Is Only a Few Early Steering Steps Away [97.11976870616273]
  We propose a lightweight inference-time defense that treats safety recovery as a satising constraint rather than an objective.<n>In our evaluations across six open-source MLRMs and four jailbreak benchmarks, SafeThink reduces attack success rates by 30-60%.
  arXiv  Detail & Related papers  (2026-02-11T18:09:17Z)
• Evaluating the Robustness of Large Language Model Safety Guardrails Against Adversarial Attacks [0.0]
  Large Language Model (LLM) safety guardrail models have emerged as a primary defense mechanism against harmful content generation.<n>This study evaluated ten publicly available guardrail models from Meta, Google, IBM, NVIDIA, Alibaba, and Allen AI across 1,445 test prompts spanning 21 attack categories.
  arXiv  Detail & Related papers  (2025-11-27T03:01:09Z)
• Eigen-1: Adaptive Multi-Agent Refinement with Monitor-Based RAG for Scientific Reasoning [53.45095336430027]
  We develop a unified framework that combines implicit retrieval and structured collaboration.<n>On Humanity's Last Exam (HLE) Bio/Chem Gold, our framework achieves 48.3% accuracy.<n>Results on SuperGPQA and TRQA confirm robustness across domains.
  arXiv  Detail & Related papers  (2025-09-25T14:05:55Z)
• Safety Pretraining: Toward the Next Generation of Safe AI [68.99129474671282]
  We present a data-centric pretraining framework that builds safety into the model from the start.<n>Our framework consists of four key steps: Safety Filtering, Safety Rephrasing, Native Refusal and Harmfulness-Tag annotated pretraining.<n>Our safety-pretrained models reduce attack success rates from 38.8% to 8.4% on standard LLM safety benchmarks with no performance on general degradation tasks.
  arXiv  Detail & Related papers  (2025-04-23T17:58:08Z)
• Benchmarking Reasoning Robustness in Large Language Models [76.79744000300363]
  We find significant performance degradation on novel or incomplete data.<n>These findings highlight the reliance on recall over rigorous logical inference.<n>This paper introduces a novel benchmark, termed as Math-RoB, that exploits hallucinations triggered by missing information to expose reasoning gaps.
  arXiv  Detail & Related papers  (2025-03-06T15:36:06Z)
• Cybersecurity Defenses: Exploration of CVE Types through Attack Descriptions [1.0474508494260908]
  VULDAT is a classification tool using a sentence transformer MPNET to identify system vulnerabilities from attack descriptions. Our model was applied to 100 attack techniques from the ATT&CK repository and 685 issues from the CVE repository. Our findings indicate that our model achieves the best performance with F1 score of 0.85, Precision of 0.86, and Recall of 0.83.
  arXiv  Detail & Related papers  (2024-07-09T11:08:35Z)
• How secure is AI-generated Code: A Large-Scale Comparison of Large Language Models [3.4887856546295333]
  This study compares state-of-the-art Large Language Models (LLMs) on their tendency to generate vulnerabilities when writing C programs.<n>At least 62.07% of the generated programs are vulnerable.
  arXiv  Detail & Related papers  (2024-04-29T01:24:14Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.