論文の概要: Multi-Pass Targeted Dynamic Symbolic Execution

• arxiv url: http://arxiv.org/abs/2408.07797v1
• Date: Wed, 14 Aug 2024 20:14:59 GMT
• ステータス: 処理完了
• システム内更新日: 2024-08-16 15:38:42.368798
• Title: Multi-Pass Targeted Dynamic Symbolic Execution
• Title（参考訳）: マルチパス目標動的シンボリック実行
• Authors: Tuba Yavuz,
• Abstract要約: 本稿では、ターゲットプログラム位置から始まり、特定のエントリポイントに到達するまで後退するマルチパスターゲット動的実行手法を提案する。 提案手法は,探索経路数の平均4倍の削減と2倍の高速化を実現する。
• 参考スコア（独自算出の注目度）: 0.0
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Dynamic symbolic execution (DSE) provides a precise means to analyze programs and it can be used to generate test cases and to detect a variety of bugs including memory vulnerabilities. However, the path explosion problem may prevent a symbolic executor from covering program locations or paths of interest. In this paper, we present a Multi-Pass Targeted Dynamic Symbolic Execution approach that starts from a target program location and moves backward until it reaches a specified entry point to check for reachability, to detect bugs on the feasible paths between the entry point and the target, and to collect constraints about the memory locations accessed by the code. Our approach uses a mix of backward and forward reasoning passes. It introduces an abstract address space that gets populated during the backward pass and uses unification to precisely map the abstract objects to the objects in the concrete address space. We have implemented our approach in a tool called DESTINA using KLEE, a DSE tool. We have evaluated DESTINA using SvComp benchmarks from the memory safety and control-flow categories. Results show that DESTINA can detect memory vulnerabilities precisely and it can help DSE reach target locations faster when it struggles with the path explosion. Our approach achieves on average 4X reduction in the number of paths explored and 2X speedup.
• Abstract（参考訳）: 動的シンボリック実行(DSE)は、プログラムを分析するための正確な手段を提供し、テストケースの生成や、メモリの脆弱性を含むさまざまなバグの検出に使用できる。 しかし、経路爆発問題は、象徴的な実行者がプログラムの場所や興味ある経路をカバーすることを妨げる可能性がある。 本稿では,対象のプログラム位置から始まり,特定のエントリポイントに到達するまで後退して到達性を確認し,エントリポイントとターゲット間の実行可能なパス上のバグを検出し,コードによってアクセスされるメモリ位置に関する制約を収集するマルチパス動的シンボル実行手法を提案する。 私たちのアプローチは、後方と前方の推論パスの混合を使用します。 これは、後方通過中に集約される抽象アドレス空間を導入し、統一を使用して抽象オブジェクトを具体的なアドレス空間内のオブジェクトに正確にマッピングする。 我々は,DSEツールであるKLEEを用いて,DESTINAと呼ばれるツールにアプローチを実装した。 メモリ安全性と制御フローのカテゴリからSvCompベンチマークを用いてDESTINAを評価した。 結果は、DESTINAがメモリの脆弱性を正確に検出できることを示し、パスの爆発に苦しむ場合、DSEがターゲット位置に到達するのを早くするのに役立つことを示している。 提案手法は,探索経路数の平均4倍の削減と2倍の高速化を実現する。

関連論文リスト

• 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)
• RTracker: Recoverable Tracking via PN Tree Structured Memory [71.05904715104411]
  本稿では,木構造メモリを用いてトラッカーと検出器を動的に関連付け,自己回復を可能にするRTrackerを提案する。 具体的には,正負と負のターゲットサンプルを時系列に保存し,維持する正負のツリー構造メモリを提案する。 我々の中核となる考え方は、正と負の目標カテゴリーの支持サンプルを用いて、目標損失の信頼性評価のための相対的距離に基づく基準を確立することである。
  論文  参考訳（メタデータ） (2024-03-28T08:54:40Z)
• Right Place, Right Time! Towards ObjectNav for Non-Stationary Goals [55.581423861790945]
  本研究では,屋内環境における非定常的かつ隠蔽されたターゲットに対して,ObjectNavタスクに取り組むための新しい手法を提案する。 本稿では,新しいメモリ拡張 LLM ベースのポリシーを用いて,その定式化,実現可能性,ナビゲーションベンチマークを提案する。
  論文  参考訳（メタデータ） (2024-03-14T22:33:22Z)
• Rampo: A CEGAR-based Integration of Binary Code Analysis and System Falsification for Cyber-Kinetic Vulnerability Detection [14.7195342186018]
  Rampoはバイナリコード解析を行い、CPS内のサイバーキネティックな脆弱性を識別する。 当社のツールは,同じ数の脆弱性を計算しながら,3倍から98倍のスピードアップを実現しています。
  論文  参考訳（メタデータ） (2024-02-20T01:36:08Z)
• SparseTrack: Multi-Object Tracking by Performing Scene Decomposition based on Pseudo-Depth [84.64121608109087]
  2次元画像から目標の相対的な深さを求めるための擬似深度推定法を提案する。 次に,得られた深度情報を用いて,高密度なターゲットセットを複数のスパースなターゲットサブセットに変換するディープカスケードマッチング(DCM)アルゴリズムを設計する。 擬似深度法とDCM戦略をデータアソシエーションプロセスに統合することにより、SparseTrackと呼ばれる新しいトラッカーを提案する。
  論文  参考訳（メタデータ） (2023-06-08T14:36:10Z)
• SalienDet: A Saliency-based Feature Enhancement Algorithm for Object Detection for Autonomous Driving [160.57870373052577]
  未知の物体を検出するために,サリエンデット法(SalienDet)を提案する。 我々のSaienDetは、オブジェクトの提案生成のための画像機能を強化するために、サリエンシに基づくアルゴリズムを利用している。 オープンワールド検出を実現するためのトレーニングサンプルセットにおいて、未知のオブジェクトをすべてのオブジェクトと区別するためのデータセットレザベリングアプローチを設計する。
  論文  参考訳（メタデータ） (2023-05-11T16:19:44Z)
• SegmentMeIfYouCan: A Benchmark for Anomaly Segmentation [111.61261419566908]
  ディープニューラルネットワーク(DNN)は通常、閉集合のセマンティッククラスで訓練される。 未発見のオブジェクトを扱うには不備だ。 このような物体の検出と局在化は、自動運転の認識などの安全クリティカルなアプリケーションに不可欠です。
  論文  参考訳（メタデータ） (2021-04-30T07:58:19Z)
• Target-Aware Object Discovery and Association for Unsupervised Video Multi-Object Segmentation [79.6596425920849]
  本稿では,教師なしビデオマルチオブジェクトセグメンテーションの課題について述べる。 より正確で効率的な時間区分のための新しいアプローチを紹介します。 DAVIS$_17$とYouTube-VISに対する提案手法を評価した結果,セグメント化精度と推論速度の両方において最先端の手法より優れていることが示された。
  論文  参考訳（メタデータ） (2021-04-10T14:39:44Z)
• An Exploration of Target-Conditioned Segmentation Methods for Visual Object Trackers [24.210580784051277]
  境界ボックストラッカーをセグメント化トラッカーに変換する方法を示す。 この手法は,最近提案されたセグメンテーショントラッカーと競合することを示す。
  論文  参考訳（メタデータ） (2020-08-03T16:21:18Z)

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

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