Skip to content

Add Tool: RAPx #444

@DiuDiu777

Description

@DiuDiu777

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

  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.
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
  1. 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.
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

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.

Metadata

Metadata

Assignees

No one assigned

    Labels

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions