-
Notifications
You must be signed in to change notification settings - Fork 57
Description
Tool Name
RAPx (Rust Analysis Platform with Extensions)
Description
RAPx is a static analysis platform for Rust. It has a specialized verification module for unsafe Rust code that systematically prevents undefined behavior (UB) through three core capabilities:
-
Audit Unit Generation: Segment code into verifiable units by analyzing unsafe code propagation patterns
-
Safety Property Verification: Use contract-based abstract interpretation to validate safety properties
-
Safety Property Inference: Automatically infers required safety conditions for unsafe APIs
For comprehensive methodology details and practical examples, see the module of verification in RAPx-Book.
Tool Information
- Does the tool perform Rust verification?
Yes – RAPx operates on Rust MIR and uses abstract interpretation to verify safety properties.
- Does the tool deal with unsafe Rust code?
Yes – RAPx has a module specializing in unsafe code audit and verification.
- Does the tool run independently in CI?
Yes – RAPx can be easily integrated into CI workflows
- Is the tool open source?
Yes –Source available on Artisan-Lab/RAPx.
- Is the tool under development?
Yes – RAPx is still under development to improve the coverage of safety properties verification.
- Will you or your team be able to provide support for the tool?
Yes – Our team, Artisan Lab at Fudan University, will offer support for issues and maintenance.
Comparison to Other Approved Tools
RAPx specializes in sound unsafe code verification through a unique methodology distinct from other Rust verification tools. While tools like Kani and GOTO Transcoder rely on SAT / SMT solver for verification, RAPx uses tags + static abstract interpretation to achieve lightweight yet complete soundness verification. The core target is verifying that unsafety is fully encapsulated or annotated in audit units– not by solving constraints, but by proving all unsafety propagations are contained under our underlying propagation assumption.
The core innovation centers on Audit Unit-guided contract verification:
-
Safety Contracts via tag-std: Leverages a standardized taxonomy of pre-defined safety properties for unsafe operations
-
Vulnerable Path Analysis: Systematically examines all execution paths in safe functions that call unsafe operations
-
Contract Satisfaction Proof: For each unsafe callee, abstract interpretation verifies its required safety contracts are fully satisfied by the current program state
Licenses
RAPx uses the MPL-2.0 license so that it's compatible with Rust’s standard library license(s).
Steps to Use the Tool
- Install
nightly-2025-06-02
on which rapx is compiled with. This just needs to do once on your machine. If the toolchain exists, this will do nothing.
rustup toolchain install nightly-2025-06-02 --profile minimal --component rustc-dev,rust-src,llvm-tools-preview
cargo +nightly-2025-06-02 install rapx --git https://github.com/Artisan-Lab/RAPx.git
- Navigate to your Rust project folder containing a
Cargo.toml
file and export the environment variable to pre-annotatedstd
. Then runrapx
and pass the-Zbuild-std
argument.
cd /to-be-verified-crate/
export RUSTUP_TOOLCHAIN=nightly-2025-06-02
export __CARGO_TESTS_ONLY_SRC_ROOT=/path-to-pre-annotated-std-lib/library
// In Linux
cargo +nightly-2025-06-02 rapx -verify -- -Zbuild-std=panic_abort,core,std --target x86_64-unknown-linux-gnu
// In Mac(Arm)
cargo +nightly-2025-06-02 rapx -verify -- -Zbuild-std=panic_abort,core,std --target aarch64-apple-darwin
Artifacts & Audit Mechanisms
-
Research Foundation:
Versioning & CI
RAPx follows semantic versioning with stable releases published on crates.io. Each version is tied to a specific Rust nightly toolchain.
The CI process is roughly as follows:
-
The verification workflow begins by installing the pinned Rust toolchain and RAPx via cargo install rapx, followed by cloning the pre-annotated tag-std safety contracts.
-
Execution targets are identified through predefined scripts that select functions in challenges.
-
The workflow runs command of verification, generating audit reports with verified safety contracts, vulnerable path coverage statistics, and undefined behavior risk diagnostics.