論文の概要: Directed Symbolic Execution for Vulnerability Discovery: An LLM-Guided Approach in KLEE

• arxiv url: http://arxiv.org/abs/2607.21676v1
• Date: Thu, 23 Jul 2026 10:54:56 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-07-27 20:58:56.955008
• Title: Directed Symbolic Execution for Vulnerability Discovery: An LLM-Guided Approach in KLEE
• Title（参考訳）: 脆弱性発見のためのシンボリック直接実行:KLEEにおけるLCMガイドによるアプローチ
• Abstract要約: シンボル的実行は、セキュリティ違反を効果的に発見するが、パスの爆発に苦しむ。 我々は,KLEE上に構築されたLarge Language Model (LLM) 誘導型シンボル実行手法であるKLEECopilotを提案する。 KLEECopilotはLSMを使用して潜在的に脆弱なコードとガイドパスの優先順位付けをマークする。 また、ループ出力優先順位付けを統合して、潜在的に脆弱性のないサイクルを回避し、より深い脆弱性に向かって進む。
• 参考スコア（独自算出の注目度）: 4.690705082550861
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Symbolic execution effectively discovers security violations but suffers from path explosion. Engines like KLEE therefore use path prioritization heuristics to order state exploration, typically optimizing code coverage. However, path prioritization can become trapped in cyclic control-flow regions, where repeated branching consumes the exploration budget before exploration reaches vulnerable code beyond these cyclic regions. We propose KLEECopilot, a Large Language Model (LLM)-guided directed symbolic execution approach built on KLEE. KLEECopilot uses LLMs to mark potentially vulnerable code and guide path prioritization. It also integrates loop-exit prioritization to escape potentially non-vulnerable cycles and progress toward deeper vulnerabilities. Compared with baselines such as Empc, KLEECopilot improves basic block coverage by 42.24% and line coverage by 125.82%. It discovers 1,335 total violations and 87 unique violations, outperforming the second-best baseline by 32.2% in total violations and Empc by 24.3% in unique violations. Although KLEECopilot is sensitive to model family, it exhibits only marginal sensitivity to model scale, supporting the efficacy of integrating security semantics and loop-exit prioritization. Ablation studies further show that individual components contribute to effectiveness: alternative configurations involving searchers, internal components, marking sources, and prompt variants yield only 54--61 unique violations, while KLEECopilot maintains competitive code coverage.
• Abstract（参考訳）: シンボル的実行は、セキュリティ違反を効果的に発見するが、パスの爆発に苦しむ。 したがって、KLEEのようなエンジンは、パス優先のヒューリスティックを使用して状態探索を順序付けし、典型的にはコードカバレッジを最適化する。 しかし、経路優先化は循環制御フロー領域に閉じ込められ、繰り返し分岐はこれらの循環領域を越えて脆弱なコードに到達する前に探索予算を消費する。 我々は,KLEE上に構築されたLarge Language Model (LLM) 誘導型シンボル実行手法であるKLEECopilotを提案する。 KLEECopilotはLSMを使用して潜在的に脆弱なコードとガイドパスの優先順位付けをマークする。 また、ループ出力優先順位付けを統合して、潜在的に脆弱性のないサイクルを回避し、より深い脆弱性に向かって進む。 Empcのようなベースラインと比較して、KLEECopilotは基本ブロックカバレッジを42.24%改善し、ラインカバレッジを125.82%改善した。 合計1,335件の違反と87件の独特な違反を発見し、総違反で32.2%、独自の違反でEmpcを24.3%上回った。 KLEECopilotはモデルファミリーに敏感であるが、モデルスケールに対する限界感度のみを示し、セキュリティセマンティクスの統合とループ排他優先順位付けの有効性をサポートする。 KLEECopilotは競争力のあるコードカバレッジを維持しているのに対して、検索者、内部コンポーネント、マーキングソース、プロンプト変種は54--61のユニークな違反しか生じない。

関連論文リスト

• EvoSafeHarness: Evolving Model- and Domain-Specific Harnesses for Securing Agents [74.54929751174289]
  EvoSafeHarnessは、ターゲットドメイン内の凍結モデルのためのデプロイ可能なハーネスを合成する、安全固有の最適化フレームワークである。 これは平均攻撃成功率を3.3ポイントのユーティリティコストで45.6%から10.0%に下げる。 また、Agent-SafetyBenchでは、すべての犠牲者に対してベストスコアを獲得している。
  論文  参考訳（メタデータ） (2026-09-05T05:56:41Z)
• CockpitHAT: Dependency-Graph-Driven Hierarchical Attribution for Embodied Multi-Agent Cockpits [3.9502278152528625]
  LLMマルチエージェントシステムは、タスクレベルの精度が高いプロセスレベルの障害を隠蔽する、正確性崩壊に悩まされる。 我々は、位置対応ウィンドウをDAGの依存性依存閾値に置き換える階層的属性フレームワークであるCockpitHATを紹介する。 CockpitBenchは、212の注釈付き障害トレースのベンチマークで、対話、車両状態、環境重大度、メモリチャネルにまたがる。
  論文  参考訳（メタデータ） (2026-08-03T07:13:00Z)
• The Geometry of Refusal: Linear Instability in Safety-Aligned LLMs [1.4323566945483497]
  我々は、"拒絶方向"を分離するゼロ最適化フレームワークであるContrastive Logit Steering (CLS)を紹介した。 CLSは出力分布を直接操作し、アライメントの診断プローブとして機能する。 7つのモデルファミリーに関する実験により、安全実装がアーキテクチャ上決定論的であることが判明した。
  論文  参考訳（メタデータ） (2026-06-21T22:04:48Z)
• Calibration Without Comprehension: Diagnosing the Limits of Fine-Tuning LLMs for Vulnerability Detection in Systems Software [1.0026496861838445]
  CWE-Traceは、手動でキュレートされたLinuxカーネルサンプルから構築された脆弱性検出フレームワークである。 対象でない検出,ターゲット検出,CWE分類において,8つのバニラLLMと15のLORA微調整変異体を評価した。
  論文  参考訳（メタデータ） (2026-06-18T17:19:26Z)
• Output Type Before Quality: A Standards-Derived XAI Admissibility Rubric for Autonomous-Driving Safety [0.4958589793470846]
  MLベースの自律運転の安全基準は、保証事例が含まなければならない証拠の種類を規定している(直接因果連鎖、定量化された介入効果、根因変数)。 しかし、XAI文献は出力型と技法系(相性マップ、特徴属性、反事実、因果グラフ、言語トレース)で整理されている。 私たちはこのミスマッチをエビデンスタイプのギャップと呼んでいます。 安全保証のためのXAI手法の選択は,メソッドの人気ではなく,ライフサイクル段階のエビデンス要求によって行うべきである。
  論文  参考訳（メタデータ） (2026-06-03T21:37:52Z)
• CauTion: Knowing When to Trust LLMs for Ensemble Causal Discovery [51.07538881798502]
  大規模言語モデル(LLM)は、統計的推論を補完する将来的なドメイン知識の源を提供する。 我々は、LLMドメイン知識を統計的因果探索アルゴリズムのアンサンブルに確実に統合するフレームワークであるCauTionを提案する。 CauTionは、データ中心とLLM拡張ベースラインの両方を一貫して上回る。
  論文  参考訳（メタデータ） (2026-06-02T13:07:43Z)
• Claw-Eval: Toward Trustworthy Evaluation of Autonomous Agents [66.97968363332465]
  エージェントベンチマークの3つのギャップに対処するエンドツーエンド評価スイートであるClaw-Evalを紹介した。 Claw-Evalは3つのグループにまたがる9つのカテゴリにまたがる300の人間検証タスクで構成されている。 すべてのエージェントアクションは、3つの独立したエビデンスチャネルを通じて記録される。
  論文  参考訳（メタデータ） (2026-04-07T17:43:18Z)
• 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)
• Improving Search Agent with One Line of Code [68.58667107354253]
  ツールベースのエージェント強化学習(TARL)は,検索エージェントが外部ツールと対話できるようにトレーニングするための,有望なパラダイムとして登場した。 textbfSearch textbfAgent textbfPolicy textbfOptimization (textbfSAPO)を提案する。
  論文  参考訳（メタデータ） (2026-03-10T04:07:39Z)
• AOI: Turning Failed Trajectories into Training Signals for Autonomous Cloud Diagnosis [19.899469614370478]
  大規模言語モデル(LLM)エージェントは、SRE(Site Reliability Engineering)を自動化するための有望なデータ駆動型アプローチを提供する 本稿では,セキュリティ制約下での構造化軌道学習問題として,自動操作を定式化したトレーニング可能なマルチエージェントフレームワークAOIを提案する。
  論文  参考訳（メタデータ） (2026-03-03T02:57:33Z)
• On GRPO Collapse in Search-R1: The Lazy Likelihood-Displacement Death Spiral [59.14787085809595]
  この障害を引き起こす中核的なメカニズムとしてLazy Likelihood Displacement(LLD)を同定する。 LDDは早期に出現し、自己強化性LDDデススパイラル(LDD Death Spiral)を引き起こす。 本稿では,GRPO のための軽量な確率保存正則化 LLDS を提案する。
  論文  参考訳（メタデータ） (2025-12-03T19:41:15Z)
• Building a Foundational Guardrail for General Agentic Systems via Synthetic Data [76.18834864749606]
  LLMエージェントは、計画段階で介入するマルチステップタスクを計画できる。 既存のガードレールは主にポスト・エグゼクティブ(英語版)を運用しており、スケーリングが困難であり、計画レベルで制御可能な監督を行う余地がほとんどない。 我々は、良性軌道を合成し、カテゴリーラベル付きリスクを困難に注入し、自動報酬モデルを介して出力をフィルタリングする制御可能なエンジンであるAuraGenを紹介する。
  論文  参考訳（メタデータ） (2025-10-10T18:42:32Z)
• Boundary-to-Region Supervision for Offline Safe Reinforcement Learning [56.150983204962735]
  バウンダリ・トゥ・レギオン(Bundary-to-Region, B2R)は、コスト信号による非対称な条件付けを可能にするフレームワークである。 B2Rは、CTGを固定された安全予算の下で境界制約として再定義し、すべての実行可能な軌道のコスト分布を統一する。 実験の結果,B2Rは38項目中35項目の安全制約を満たすことがわかった。
  論文  参考訳（メタデータ） (2025-09-30T03:38:20Z)

関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。

指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。