UnsafeChecker is presented, a compiler-integrated static analysis framework for detecting potential soundness violations in Rust safe abstractions, and outperforms several state-of-the-art tools, detecting 32 CVEs and covering 36 bugs with 51.6% alert-level precision.
Abstract
Rust guarantees memory safety without garbage collection through a strict ownership and borrowing system. However, for low-level systems programming, many widely used libraries rely on the unsafe keyword. These libraries encapsulate raw-pointer operations behind safe APIs to form safe abstractions. A single mistake in this internal unsafe code can break its safety contract, rendering the abstraction unsound and allowing safe clients to trigger undefined behavior. Detecting these potential soundness violations is challenging. Existing static analysis tools for C/C++ ignore Rust-specific safety contracts, while current Rust tools lack the deep semantic modeling required to track the contexts that raw pointers erase. To address this gap, we present UnsafeChecker, a compiler-integrated static analysis framework for detecting potential soundness violations in Rust safe abstractions. UnsafeChecker analyzes Rust MIR using a flow-sensitive abstract interpretation that maintains a shared state with three components: ownership, object validity, and layout. Each warning rule consumes the subset of facts needed for the corresponding Rust safety obligation. UnsafeChecker reports both instruction-level undefined behavior and boundary-level contract violations that may escape through safe APIs. We evaluate UnsafeChecker on a benchmark of 46 RustSec vulnerabilities, which contain 53 ground-truth bugs. UnsafeChecker outperforms several state-of-the-art tools, detecting 32 CVEs and covering 36 bugs (67.9% recall) with 51.6% alert-level precision. Furthermore, in a large-scale scan of real-world crates on crates.io, UnsafeChecker uncovered 114 previously unknown bugs across 83 crates, with 45 confirmed and 27 already fixed by maintainers.
Rust has emerged as a promising systems programming language for security-critical domains, offering effective protection against memory safety issues through its strong type system and ownership model. However, practical multilingual Rust applications that interact with unsafe languages such as C/C++ via the Foreign F...
Ming-Liang Liu, Bao-Jian Hua· International Test Conferenc...· 0 citations
Rust has emerged as the leading system programming language, offering strong memory and type safety guarantees without compromising performance. This positions it as a compelling alternative to traditional languages like C and C++, which are susceptible to memory security bugs. However, manually transforming C to Rust...
Memory safety is a dominant driver in security and systems research. Rust has become a viable alternative to C/C++ for systems programming because of its strong memory safety guarantees. However, it is not a silver bullet. Unsafe sections, foreign code, and compiler-soundness bugs still pose vulnerabilities. Compartmen...
Maxim Ritter von Onciul, Phillip Raffeck, Peter Wägemann et al.· Proceedings of the 14th Work...· 0 citations
How to extend RefinedRust with several of the high-level abstractions that Rust provides, including traits, closures, and iterators, and in a manner such that they can be used in conjunction with unsafe code.
Lennard Gäher, Vincent Lafeychine, Sascha Kehrli et al.· Proceedings of the ACM on Pr...· 0 citations
Rust is increasingly used as a viable alternative to C and C++ for systems development. A central appeal of Rust is its “zero-cost” abstractions and, specifically, its ability to enforce safety without the overhead of garbage collection. In practice, however, only a subset of safety properties can be enforced staticall...
Soham Bagchi, Manvik Nanda, A. Burtsev· Proceedings of the 14th Work...· 0 citations
This work evaluates three commit-time guard granularities (global epoch, read-set version, semantic commit predicate), multi-level verification, and model-side gates on three locally hosted quantized model families, and investigates how precisely runtime guards distinguish invalidating races.
Zi-Hao Zheng, Jia-Yu Long, Bai-Chuan Li et al.· 0 citations
We use cookies to run the site and, with your consent, for analytics and to show ads.
See our Cookie Policy.