論文の概要: Petri Nets-based Methods on Automatically Detecting for Concurrency Bugs in Rust Programs

• arxiv url: http://arxiv.org/abs/2212.02754v3
• Date: Tue, 23 Sep 2025 00:55:32 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-09-24 20:41:27.336292
• Title: Petri Nets-based Methods on Automatically Detecting for Concurrency Bugs in Rust Programs
• Title（参考訳）: ペトリネットを用いたRustプログラムにおける並行バグの自動検出手法
• Authors: Kaiwen Zhang, Guanjun Liu,
• Abstract要約: 本稿では,Rustのバグを効率よく,高精度に検出するペトリネット方式を提案する。 中心となるイノベーションは、Rustのオーナシップセマンティクスと同期プリミティブの厳格でコントロールフロー駆動のモデリングである。 LockBudと比較して、私たちのアプローチは偽陽性を35.7%、偽陰性を28.3%削減します。
• 参考スコア（独自算出の注目度）: 5.064868362565062
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Rust's memory safety guarantees, notably ownership and lifetime systems, have driven its widespread adoption. Concurrency bugs still occur in Rust programs, and existing detection approaches exhibit significant limitations: static analyzers suffer from context insensitivity and high false positives, while dynamic methods incur prohibitive runtime costs due to exponential path exploration. This paper presents a Petri net-based method for efficient, precise detection of Rust concurrency bugs. The method rests on three pillars: (1) A syntax-preserving program-to-Petri-net transformation tailored for target bug classes; (2) Semantics-preserving state compression via context-aware slicing; (3) Bug detection through efficient Petri net reachability analysis. The core innovation is its rigorous, control-flow-driven modeling of Rust's ownership semantics and synchronization primitives within the Petri net structure, with data operations represented as token movements. Integrated pointer analysis automates alias identification during transformation. Experiments on standard Rust concurrency benchmarks demonstrate that our method outperforms the state-of-the-art methods LockBud and Miri that are both tools of detecting concurrency bugs of Rust programs. Compared to LockBud, our approach reduces false positives by 35.7\% and false negatives by 28.3\% , which is obtained through our precise flow-sensitive pointer analysis. Compared with Miri that is a dynamic analysis tool, although Miri can obtain the same detection results, our method achieves 100% faster verification speed since our method takes a state reduce algorithm.
• Abstract（参考訳）: Rustのメモリ安全性保証、特にオーナシップとライフタイムシステムは、広く採用されている。 静的アナライザはコンテキスト不感度と高い偽陽性に悩まされ、動的メソッドは指数パス探索による禁止実行コストを発生させる。 本稿では,Rust並列性バグを効率よく,高精度に検出するペトリネット方式を提案する。 本手法は,(1)目標となるバグクラスに適した構文保存型プログラム・ツー・ペトリネット変換,(2)コンテキスト認識スライシングによる意味保存型状態圧縮,(3)ペトリネットの効率的な到達性解析によるバグ検出の3つの柱に留まる。 中心となるイノベーションは、Rustのオーナシップセマンティクスとペトリネット構造内の同期プリミティブの厳格で制御フロー駆動のモデリングであり、データ操作はトークンのムーブメントとして表現されている。 統合ポインタ解析は変換中のエイリアス識別を自動化する。 Rustの並列性ベンチマークの実験では、私たちのメソッドは、Rustプログラムの並行性バグを検出するツールであるLockBudとMiriの最先端メソッドよりも優れています。 LockBudと比較して、我々のアプローチは、正確なフローセンシティブなポインタ分析によって得られた偽陽性を35.7\%、偽陰性を28.3\%削減する。 動的解析ツールである Miri と比較すると,Mari は同じ検出結果が得られるが,本手法ではステートリダクションアルゴリズムを採用しているため,検証速度が100%向上する。

関連論文リスト

• Deep Learning Based Concurrency Bug Detection and Localization [9.2389985253336]
  並行性バグは、ソフトウェアの信頼性とセキュリティを検知し、妥協することが難しいことで知られている。 既存のディープラーニング手法には3つの大きな制限がある。 そこで本研究では,効率的なバグ検出とローカライゼーションのための新しい手法を提案する。
  論文  参考訳（メタデータ） (2025-08-28T15:40:20Z)
• MIB: A Mechanistic Interpretability Benchmark [77.35046700898326]
  4つのタスクと5つのモデルにまたがる2つのトラックを持つメカニスティック解釈可能性ベンチマークMIBを提案する。 MIBを用いて、帰属とマスク最適化の手法が回路のローカライゼーションにおいて最適であることがわかった。 因果変数の局在化では、教師付きDAS法がニューロンより優れているが、SAEの特徴はニューロンより優れている。
  論文  参考訳（メタデータ） (2025-04-17T17:55:45Z)
• Static Deadlock Detection for Rust Programs [6.596623081054982]
  Rustはスレッドとメモリの安全性を確保するために独自のオーナシップメカニズムに依存している。 Rustの新しい言語機能は、脆弱性検出に新たな課題をもたらす。 本稿では,Rustプログラムに適した静的デッドロック検出手法を提案する。
  論文  参考訳（メタデータ） (2024-01-02T09:09:48Z)
• Yuga: Automatically Detecting Lifetime Annotation Bugs in the Rust Language [15.164423552903571]
  Rustプロジェクトでは、セキュリティ上の脆弱性が報告されている。 これらの脆弱性は、部分的には関数シグネチャの誤った終身アノテーションから生じます。 既存のツールはこれらのバグを検出するのに失敗する。 我々は,新たな静的解析ツールであるYugaを考案し,潜在的なライフタイムアノテーションのバグを検出する。
  論文  参考訳（メタデータ） (2023-10-12T17:05:03Z)
• Confidence-aware Training of Smoothed Classifiers for Certified Robustness [75.95332266383417]
  我々は「ガウス雑音下での精度」を、入力に対する対角的ロバスト性の容易に計算可能なプロキシとして利用する。 実験の結果, 提案手法は, 最先端の訓練手法による信頼性向上を継続的に示すことがわかった。
  論文  参考訳（メタデータ） (2022-12-18T03:57:12Z)
• Manifold Regularized Dynamic Network Pruning [102.24146031250034]
  本稿では,全インスタンスの多様体情報をプルーンドネットワークの空間に埋め込むことにより,冗長フィルタを動的に除去する新しいパラダイムを提案する。 提案手法の有効性をいくつかのベンチマークで検証し,精度と計算コストの両面で優れた性能を示す。
  論文  参考訳（メタデータ） (2021-03-10T03:59:03Z)
• CIMON: Towards High-quality Hash Codes [63.37321228830102]
  我々はtextbfComprehensive stextbfImilarity textbfMining と ctextbfOnsistency leartextbfNing (CIMON) という新しい手法を提案する。 まず、グローバルな洗練と類似度統計分布を用いて、信頼性とスムーズなガイダンスを得る。第二に、意味的整合性学習とコントラスト的整合性学習の両方を導入して、乱不変と差別的ハッシュコードの両方を導出する。
  論文  参考訳（メタデータ） (2020-10-15T14:47:14Z)

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

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