論文の概要: Empc: Effective Path Prioritization for Symbolic Execution with Path Cover

• arxiv url: http://arxiv.org/abs/2505.03555v1
• Date: Tue, 06 May 2025 14:08:36 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-05-07 18:50:11.414662
• Title: Empc: Effective Path Prioritization for Symbolic Execution with Path Cover
• Title（参考訳）: Empc: 経路被覆を伴うシンボリック・エクセプションの効果的な経路優先化
• Authors: Shuangjie Yao, Dongdong She,
• Abstract要約: 記号的実行は、プログラムの動作の正しさを正式に推論し、ソフトウェアバグを検出する。 それは固有の限界、すなわち経路の爆発に悩まされる。 本稿では,Empcという経路被覆を用いた新規かつ効果的な経路優先順位付け手法を提案する。
• 参考スコア（独自算出の注目度）: 4.247960711260534
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Symbolic execution is a powerful program analysis technique that can formally reason the correctness of program behaviors and detect software bugs. It can systematically explore the execution paths of the tested program. But it suffers from an inherent limitation: path explosion. Path explosion occurs when symbolic execution encounters an overwhelming number (exponential to the program size) of paths that need to be symbolically reasoned. It severely impacts the scalability and performance of symbolic execution. To tackle this problem, previous works leverage various heuristics to prioritize paths for symbolic execution. They rank the exponential number of paths using static rules or heuristics and explore the paths with the highest rank. However, in practice, these works often fail to generalize to diverse programs. In this work, we propose a novel and effective path prioritization technique with path cover, named Empc. Our key insight is that not all paths need to be symbolically reasoned. Unlike traditional path prioritization, our approach leverages a small subset of paths as a minimum path cover (MPC) that can cover all code regions of the tested programs. To encourage diversity in path prioritization, we compute multiple MPCs. We then guide the search for symbolic execution on the small number of paths inside multiple MPCs rather than the exponential number of paths. We implement our technique Empc based on KLEE. We conduct a comprehensive evaluation of Empc to investigate its performance in code coverage, bug findings, and runtime overhead. The evaluation shows that Empc can cover 19.6% more basic blocks than KLEE's best search strategy and 24.4% more lines compared to the state-of-the-art work cgs. Empc also finds 24 more security violations than KLEE's best search strategy. Meanwhile, Empc can significantly reduce the memory usage of KLEE by up to 93.5%.
• Abstract（参考訳）: 記号実行は、プログラムの動作の正しさを正式に推論し、ソフトウェアバグを検出する強力なプログラム解析技術である。 テストプログラムの実行パスを体系的に探索することができる。 しかし、それは本質的に限界であるパスの爆発に悩まされている。 経路の爆発は、記号的実行がシンボル的推論を必要とする経路の圧倒的な数(プログラムサイズに比例する)に遭遇した時に起こる。 これはシンボリック実行のスケーラビリティとパフォーマンスに大きな影響を与えます。 この問題に対処するために、過去の研究は様々なヒューリスティックを活用して、シンボル実行のための経路を優先順位付けした。 彼らは静的な規則やヒューリスティックを使って指数的な数のパスをランク付けし、最高ランクのパスを探索する。 しかし、実際には、これらの作品は多種多様なプログラムへの一般化に失敗することが多い。 本研究では,Empcという経路被覆を用いた新規かつ効果的な経路優先手法を提案する。 私たちの重要な洞察は、すべてのパスを象徴的に推論する必要はないということです。 従来のパス優先方式とは異なり,本手法では,テスト対象プログラムのコード領域を網羅する最小パスカバー (MPC) として,パスの小さなサブセットを利用する。 経路優先化の多様性を促進するため、複数のMPCを演算する。 次に、指数的なパス数ではなく、複数のMPC内の少数のパスのシンボリック実行の探索をガイドする。 我々はKLEEに基づくEmpcの手法を実装した。 コードカバレッジ、バグ発見、ランタイムオーバーヘッドのパフォーマンスを調査するために、Empcの包括的な評価を行います。 評価の結果、EmpcはKLEEの最良の検索戦略よりも19.6%多くの基本ブロックをカバーでき、最先端の作業cgに比べて24.4%のラインをカバーできることがわかった。 Empcはまた、KLEEの最高の検索戦略よりも24件のセキュリティ違反を発見した。 一方、EmpcはKLEEのメモリ使用量を最大93.5%削減することができる。

関連論文リスト

• Soft Reasoning Paths for Knowledge Graph Completion [63.23109723605835]
  推論パスは知識グラフ補完(KGC)における信頼できる情報である 現実のアプリケーションでは、計算に手頃なパスが全ての候補エンティティに対して存在することを保証することは困難である。 そこで本研究では,提案アルゴリズムを不備な経路状況に対してより安定にするために,ソフト推論パスを導入する。
  論文  参考訳（メタデータ） (2025-05-06T08:12:48Z)
• Vital: Vulnerability-Oriented Symbolic Execution via Type-Unsafe Pointer-Guided Monte Carlo Tree Search [18.500951309269396]
  本稿では,タイプアンセーフポインタ誘導モンテカルロ木探索(MCTS)による新たな脆弱性指向のシンボル実行を提案する。 Vitalは最大90.03%の安全でないポインタをカバーし、最大37.50%のメモリエラーを検出することができる。 後者では、Vitalは最大30倍の高速化を実現し、最大20倍のメモリ消費を削減できることを示した。
  論文  参考訳（メタデータ） (2024-08-16T14:29:57Z)
• Multi-Pass Targeted Dynamic Symbolic Execution [0.0]
  本稿では、ターゲットプログラム位置から始まり、特定のエントリポイントに到達するまで後退するマルチパスターゲット動的実行手法を提案する。 提案手法は,探索経路数の平均4倍の削減と2倍の高速化を実現する。
  論文  参考訳（メタデータ） (2024-08-14T20:14:59Z)
• Path-optimal symbolic execution of heap-manipulating programs [5.639904484784126]
  本稿では、当初、ヒープ操作プログラムに対して経路最適性を実現するシンボル実行アルゴリズムであるPOSEについて紹介する。 我々は,POSEアルゴリズムを小型で汎用的なオブジェクト指向プログラミング言語に形式化し,プロトタイプのシンボルエグゼキュータに形式化を実装し,データ構造を入力とするサンプルプログラムのベンチマークに対して,アルゴリズムを実験する。
  論文  参考訳（メタデータ） (2024-07-23T20:35:33Z)
• Finding Transformer Circuits with Edge Pruning [71.12127707678961]
  自動回路発見の効率的かつスケーラブルなソリューションとしてエッジプルーニングを提案する。 本手法は,従来の手法に比べてエッジ数の半分未満のGPT-2の回路を探索する。 その効率のおかげで、Edge PruningをCodeLlama-13Bにスケールしました。
  論文  参考訳（メタデータ） (2024-06-24T16:40:54Z)
• SLOPE: Search with Learned Optimal Pruning-based Expansion [2.0618817976970103]
  SLOPE(Learned Optimal Pruning-based Expansion)を用いた探索手法を提案する。 ノードの距離を最適経路から学習し、その結果、オープンリストのサイズを小さくする。 これにより、探索は最適な経路に近い領域のみを探索し、メモリと計算コストを削減できる。
  論文  参考訳（メタデータ） (2024-06-07T13:42:15Z)
• Parallel Program Analysis on Path Ranges [3.018638214344819]
  Ranged symbolic execution は、並列にパス範囲と呼ばれるプログラム部分でシンボリックな実行を実行する。 本稿では,プログラムを経路範囲に分割し,任意の解析を並列に行う検証手法を提案する。
  論文  参考訳（メタデータ） (2024-02-19T08:26:52Z)
• Path Choice Matters for Clear Attribution in Path Methods [84.29092710376217]
  重要でない特徴に対する高い属性を割り当てるtextbfConcentration Principleを導入する。 次に、モデルに依存しないインタプリタである textbfSAMP を提示し、ほぼ最適経路を効率的に探索する。 また、厳密性と最適性を改善するために、無限小制約(IC)と運動量戦略(MS)を提案する。
  論文  参考訳（メタデータ） (2024-01-19T01:11:44Z)
• Monte-Carlo Tree Search for Multi-Agent Pathfinding: Preliminary Results [60.4817465598352]
  マルチエージェントパスフィンディングに適したモンテカルロ木探索(MCTS)のオリジナル版を紹介する。 具体的には,エージェントの目標達成行動を支援するために,個別の経路を用いる。 また,木探索手順の分岐係数を低減するために,専用の分解手法を用いる。
  論文  参考訳（メタデータ） (2023-07-25T12:33:53Z)
• GreedyNASv2: Greedier Search with a Greedy Path Filter [70.64311838369707]
  ワンショットNAS法では、検索スペースは通常かなり大きい(例えば1321ドル)。 本稿では,明示的な経路フィルタを用いて経路の特性を抽出し,弱い経路を直接フィルタする。 例えば、取得したGreedyNASv2-Lは、ImageNetデータセットで811.1%のTop-1精度を実現し、ResNet-50の強いベースラインを著しく上回っている。
  論文  参考訳（メタデータ） (2021-11-24T16:32:29Z)
• ROME: Robustifying Memory-Efficient NAS via Topology Disentanglement and Gradient Accumulation [106.04777600352743]
  微分可能なアーキテクチャサーチ(DARTS)は、スーパーネット全体がメモリに格納されているため、メモリコストが大幅に低下する。 シングルパスのDARTSが登場し、各ステップでシングルパスのサブモデルのみを選択する。 メモリフレンドリーだが、計算コストも低い。 RObustifying Memory-Efficient NAS (ROME) と呼ばれる新しいアルゴリズムを提案する。
  論文  参考訳（メタデータ） (2020-11-23T06:34:07Z)

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

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