論文の概要: 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%向上する。
関連論文リスト
- Backdoor Collapse: Eliminating Unknown Threats via Known Backdoor Aggregation in Language Models [75.29749026964154]
Ourmethodは、複数のベンチマークで平均的な攻撃成功率を4.41%に下げる。
クリーンな精度と実用性はオリジナルのモデルの0.5%以内に保存される。
防衛はさまざまな種類のバックドアをまたいで一般化し、実際のデプロイメントシナリオにおける堅牢性を確認します。
論文 参考訳(メタデータ) (2025-10-11T15:47:35Z) - RefFilter: Improving Semantic Conflict Detection via Refactoring-Aware Static Analysis [2.4000626364733684]
RefFilterは意味的干渉検出のためのSDG対応ツールである。
精度を向上させるために自動検出を統合することで、既存の静的技術の上に構築される。
その結果、ラベル付きデータセットでは、RefFilterは偽陽性を約32%削減している。
論文 参考訳(メタデータ) (2025-10-02T12:30:49Z) - Beyond Embeddings: Interpretable Feature Extraction for Binary Code Similarity [3.9488518969307305]
言語モデルに基づくエージェントを用いて、アセンブリコードの構造化推論分析を行う。
手作りの機能とは違って、よりリッチで適応性がある。埋め込みとは違い、人間可読性があり、保守性があり、逆あるいはリレーショナルインデックスで直接検索できる。
論文 参考訳(メタデータ) (2025-09-27T18:34:32Z) - Deep Learning Based Concurrency Bug Detection and Localization [9.2389985253336]
並行性バグは、ソフトウェアの信頼性とセキュリティを検知し、妥協することが難しいことで知られている。
既存のディープラーニング手法には3つの大きな制限がある。
そこで本研究では,効率的なバグ検出とローカライゼーションのための新しい手法を提案する。
論文 参考訳(メタデータ) (2025-08-28T15:40:20Z) - CRUST-Bench: A Comprehensive Benchmark for C-to-safe-Rust Transpilation [51.18863297461463]
CRUST-Benchは100のCリポジトリのデータセットで、それぞれが安全なRustとテストケースで手書きのインターフェースとペアリングされている。
我々は、このタスクで最先端の大規模言語モデル(LLM)を評価し、安全で慣用的なRust生成が依然として難しい問題であることを確認した。
最高のパフォーマンスモデルであるOpenAI o1は、ワンショット設定で15タスクしか解決できない。
論文 参考訳(メタデータ) (2025-04-21T17:33:33Z) - 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)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。