# 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](https://artisan-lab.github.io/RAPx-Book/6.4-unsafe.html). # Tool Information - [x] Does the tool perform Rust verification? Yes – RAPx operates on Rust MIR and uses abstract interpretation to verify safety properties. - [x] Does the tool deal with unsafe Rust code? Yes – RAPx has a module specializing in unsafe code audit and verification. - [x] Does the tool run independently in CI? Yes – RAPx can be easily integrated into CI workflows - [x] Is the tool open source? Yes –Source available on [Artisan-Lab/RAPx](https://github.com/Artisan-Lab/RAPx). - [x] Is the tool under development? Yes – RAPx is still under development to improve the coverage of safety properties verification. - [x] 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](https://github.com/Artisan-Lab/tag-std/blob/main/primitive-sp.md): 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](https://github.com/Artisan-Lab/RAPx?tab=readme-ov-file#MPL-2.0-1-ov-file) so that it's compatible with Rust’s standard library license(s). # Steps to Use the Tool 1. 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. ```shell 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 ``` 2. Navigate to your Rust project folder containing a `Cargo.toml` file and export the environment variable to pre-annotated `std`. Then run `rapx` and pass the `-Zbuild-std` argument. ```shell 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: * Audit Unit: [Annotating and Auditing the Safety Properties of Unsafe Rust](https://arxiv.org/abs/2504.21312) # Versioning & CI RAPx follows semantic versioning with stable releases published on [crates.io](https://crates.io/crates/rapx). 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.