Petri Nets-based Methods on Automatically Detecting for Concurrency Bugs in Rust Programs

• URL: http://arxiv.org/abs/2212.02754v3
• Date: Tue, 23 Sep 2025 00:55:32 GMT
• Title: Petri Nets-based Methods on Automatically Detecting for Concurrency Bugs in Rust Programs
• Authors: Kaiwen Zhang, Guanjun Liu,
• Abstract summary: This paper presents a Petri net-based method for efficient, precise detection of Rust bugs.<n>The core innovation is its rigorous, control-flow-driven modeling of Rust's ownership semantics and synchronization primitives.<n>Compared to LockBud, our approach reduces false positives by 35.7% and false negatives by 28.3%.
• Score: 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.

Related papers

• Backdoor Collapse: Eliminating Unknown Threats via Known Backdoor Aggregation in Language Models [75.29749026964154]
  Ourmethod reduces the average Attack Success Rate to 4.41% across multiple benchmarks.<n>Clean accuracy and utility are preserved within 0.5% of the original model.<n>The defense generalizes across different types of backdoors, confirming its robustness in practical deployment scenarios.
  arXiv  Detail & Related papers  (2025-10-11T15:47:35Z)
• RefFilter: Improving Semantic Conflict Detection via Refactoring-Aware Static Analysis [2.4000626364733684]
  RefFilter is a SDG-aware tool for semantic interference detection.<n>It builds on existing static techniques by incorporating automated detection to improve precision.<n>Results show that RefFilter reduces false positives by nearly 32% on the labeled dataset.
  arXiv  Detail & Related papers  (2025-10-02T12:30:49Z)
• Beyond Embeddings: Interpretable Feature Extraction for Binary Code Similarity [3.9488518969307305]
  We use a language model-based agent to conduct structured reasoning analysis of assembly code.<n>Unlike hand-crafted features, they are richer and adaptive. Unlike embeddings, they are human-readable, maintainable, and directly searchable with inverted or relational indexes.
  arXiv  Detail & Related papers  (2025-09-27T18:34:32Z)
• Deep Learning Based Concurrency Bug Detection and Localization [9.2389985253336]
  Concurrency bugs are notoriously hard to detect and compromise software reliability and security.<n>Existing deep learning methods face three main limitations.<n>We propose a novel method for effective bug detection as well as localization.
  arXiv  Detail & Related papers  (2025-08-28T15:40:20Z)
• CRUST-Bench: A Comprehensive Benchmark for C-to-safe-Rust Transpilation [51.18863297461463]
  CRUST-Bench is a dataset of 100 C repositories, each paired with manually-written interfaces in safe Rust as well as test cases.<n>We evaluate state-of-the-art large language models (LLMs) on this task and find that safe and idiomatic Rust generation is still a challenging problem.<n>The best performing model, OpenAI o1, is able to solve only 15 tasks in a single-shot setting.
  arXiv  Detail & Related papers  (2025-04-21T17:33:33Z)
• MIB: A Mechanistic Interpretability Benchmark [77.35046700898326]
  We propose MIB, a Mechanistic Interpretability Benchmark, with two tracks spanning four tasks and five models.<n>Using MIB, we find that attribution and mask optimization methods perform best on circuit localization.<n>For causal variable localization, we find that the supervised DAS method performs best, while SAE features are not better than neurons.
  arXiv  Detail & Related papers  (2025-04-17T17:55:45Z)
• Static Deadlock Detection for Rust Programs [6.596623081054982]
  Rust relies on its unique ownership mechanism to ensure thread and memory safety. New language features in Rust pose new challenges for vulnerability detection. This paper proposes a static deadlock detection method tailored for Rust programs.
  arXiv  Detail & Related papers  (2024-01-02T09:09:48Z)
• Yuga: Automatically Detecting Lifetime Annotation Bugs in the Rust Language [15.164423552903571]
  Security vulnerabilities have been reported in Rust projects, often attributed to the use of "unsafe" Rust code.<n>These vulnerabilities, in part, arise from incorrect lifetime annotations on function signatures.<n>Existing tools fail to detect these bugs, primarily because such bugs are rare, challenging to detect through dynamic analysis.<n>We devise a novel static analysis tool, Yuga, to detect potential lifetime annotation bugs.
  arXiv  Detail & Related papers  (2023-10-12T17:05:03Z)
• Confidence-aware Training of Smoothed Classifiers for Certified Robustness [75.95332266383417]
  We use "accuracy under Gaussian noise" as an easy-to-compute proxy of adversarial robustness for an input. Our experiments show that the proposed method consistently exhibits improved certified robustness upon state-of-the-art training methods.
  arXiv  Detail & Related papers  (2022-12-18T03:57:12Z)
• Manifold Regularized Dynamic Network Pruning [102.24146031250034]
  This paper proposes a new paradigm that dynamically removes redundant filters by embedding the manifold information of all instances into the space of pruned networks. The effectiveness of the proposed method is verified on several benchmarks, which shows better performance in terms of both accuracy and computational cost.
  arXiv  Detail & Related papers  (2021-03-10T03:59:03Z)
• CIMON: Towards High-quality Hash Codes [63.37321228830102]
  We propose a new method named textbfComprehensive stextbfImilarity textbfMining and ctextbfOnsistency leartextbfNing (CIMON) First, we use global refinement and similarity statistical distribution to obtain reliable and smooth guidance. Second, both semantic and contrastive consistency learning are introduced to derive both disturb-invariant and discriminative hash codes.
  arXiv  Detail & Related papers  (2020-10-15T14:47:14Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.