論文の概要: Broken by Default: A Formal Verification Study of Security Vulnerabilities in AI-Generated Code
- arxiv url: http://arxiv.org/abs/2604.05292v2
- Date: Wed, 08 Apr 2026 16:49:43 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-04-09 14:06:05.093712
- Title: Broken by Default: A Formal Verification Study of Security Vulnerabilities in AI-Generated Code
- Title（参考訳）: デフォルトで破られた: AI生成コードのセキュリティ脆弱性の形式的検証
- Authors: Dominik Blain, Maxime Noiseux,
- Abstract要約: Broken by Defaultは、500のセキュリティクリティカルなプロンプトにまたがる7つの広くデプロイされたLLMによって生成される3500のコードアーティファクトの正式な検証研究である。
すべてのモデル全体で、55.8%のアーティファクトは少なくとも1つのCOBALT識別された脆弱性を含んでいる。
GPT-4oは62.4%(グレードF)、Gemini 2.5 Flashは48.4%(グレードD)である。
- 参考スコア（独自算出の注目度）: 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.
- Abstract（参考訳）: AIコーディングアシスタントは、セキュリティに敏感なドメインでプロダクションコードを生成するために使用されている。
セキュリティクリティカルな500のプロンプト(5つのCWEカテゴリ、それぞれ100のプロンプト)にわたる7つの広くデプロイされたLLMによって生成される3,500のコードアーティファクトの正式な検証結果です。
各アーティファクトは、COBALT分析パイプラインを介してZ3 SMTソルバの対象となり、パターンベースのヒューリスティックではなく、数学的に満足できる証人を生成する。
すべてのモデル全体で、55.8%のアーティファクトは少なくとも1つのCOBALT識別された脆弱性を含んでいる。
GPT-4oは62.4%(グレードF)、Gemini 2.5 Flashは48.4%(グレードD)である。
7つの代表的な発見のうち6つは、GCC Address Sanitizerの下で実行時のクラッシュを確認している。
1) 明示的なセキュリティ命令は平均を4ポイント減らし、(2) 業界ツールと組み合わせて97.8%のZ3証明の結果を見逃し、(3) モデルでは、レビューモードの78.7%の時点では55.8%で出力する。
関連論文リスト
- SecPI: Secure Code Generation with Reasoning Models via Security Reasoning Internalization [50.71047638695205]
RLM(Reasoning Language Model)は、プログラミングにおいてますます使われている言語モデルである。
しかし、最先端のRLMでさえ、生成されたコードに重大なセキュリティ脆弱性を頻繁に導入する。
我々は、構造化されたセキュリティ推論を内部化するためのRTMを教える微調整パイプラインであるSecPIを提案する。
論文 参考訳（メタデータ） (2026-04-04T04:29:11Z) - Credential Leakage in LLM Agent Skills: A Large-Scale Empirical Study [51.717224133855886]
サードパーティのスキルはLLMエージェントを強力な能力で拡張するが、特権のある環境では機密情報を扱うことが多い。
静的解析,サンドボックステスト,手動検査を用いて17,022のスキル(SkillsMPで170,226からサンプリング)を分析した。
我々は,1,708の課題で520の脆弱なスキルを識別し,10の漏洩パターン(事故4件,反対6件)の分類を導出する。
論文 参考訳（メタデータ） (2026-04-03T14:50:16Z) - Emergent Formal Verification: How an Autonomous AI Ecosystem Independently Discovered SMT-Based Safety Across Six Domains [0.0]
本稿では,共通APIを通じて6つの出力クラスすべてにZ3ベースの検証を適用する統一フレームワークを提案する。
提案手法を5つの実装ドメインで181のテストケースで評価し,100%の分類精度,0の偽陽性,0の偽陰性で評価した。
論文 参考訳（メタデータ） (2026-03-22T10:02:16Z) - Safety Recovery in Reasoning Models Is Only a Few Early Steering Steps Away [97.11976870616273]
本稿では,安全回復を目的ではなく満足度の高い制約として扱う軽量な推論時防衛法を提案する。
6つのオープンソースMLRMと4つのjailbreakベンチマークで評価した結果、SafeThinkは攻撃成功率を30～60%削減しました。
論文 参考訳（メタデータ） (2026-02-11T18:09:17Z) - Evaluating the Robustness of Large Language Model Safety Guardrails Against Adversarial Attacks [0.0]
大言語モデル(LLM)の安全ガードレールモデルは有害なコンテンツ生成に対する主要な防御機構として出現している。
この調査は、21の攻撃カテゴリにわたる1,445のテストプロンプトで、Meta、Google、IBM、NVIDIA、Alibaba、Allen AIから利用可能な10のガードレールモデルを評価した。
論文 参考訳（メタデータ） (2025-11-27T03:01:09Z) - Eigen-1: Adaptive Multi-Agent Refinement with Monitor-Based RAG for Scientific Reasoning [53.45095336430027]
暗黙的な検索と構造化された協調を組み合わせた統合フレームワークを開発する。
Humanity's Last Exam (HLE) Bio/Chem Goldでは,48.3%の精度を実現している。
SuperGPQAとTRQAの結果はドメイン間の堅牢性を確認した。
論文 参考訳（メタデータ） (2025-09-25T14:05:55Z) - Safety Pretraining: Toward the Next Generation of Safe AI [68.99129474671282]
モデルの安全性を最初から構築する,データ中心の事前トレーニングフレームワークを提案する。
我々のフレームワークは、セーフティフィルタリング、セーフティリフレージング、Native Refusal、Harmfulness-Tag Annotated Pretrainingの4つの重要なステップで構成されています。
我々の安全事前訓練モデルでは、一般的な劣化タスクのパフォーマンスを伴わない標準LLM安全性ベンチマークにおいて、攻撃成功率を38.8%から8.4%に下げている。
論文 参考訳（メタデータ） (2025-04-23T17:58:08Z) - Benchmarking Reasoning Robustness in Large Language Models [76.79744000300363]
新規データや不完全データでは,性能が著しく低下することがわかった。
これらの結果は、厳密な論理的推論に対するリコールへの依存を浮き彫りにした。
本稿では,情報不足によって引き起こされる幻覚を利用して推論ギャップを明らかにする,Math-RoBと呼ばれる新しいベンチマークを提案する。
論文 参考訳（メタデータ） (2025-03-06T15:36:06Z) - Cybersecurity Defenses: Exploration of CVE Types through Attack Descriptions [1.0474508494260908]
VULDATは、文変換器MPNETを使用して、攻撃記述からシステムの脆弱性を識別する分類ツールである。
また,ATT&CKレポジトリから100件,CVEレポジトリから685件のアタック手法を適用した。
以上の結果より,F1スコア0.85,精度0.86,リコール0.83,F1スコア0.83,F1スコア0.85,F1スコア0.86,F1スコア0.83,F1スコア0。
論文 参考訳（メタデータ） (2024-07-09T11:08:35Z) - How secure is AI-generated Code: A Large-Scale Comparison of Large Language Models [3.4887856546295333]
本研究では,C言語記述時の脆弱性発生傾向について,最先端のLarge Language Model (LLM)を比較した。
生成されたプログラムの少なくとも62.07%は脆弱性がある。
論文 参考訳（メタデータ） (2024-04-29T01:24:14Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。