A curated list of awesome Rust checkers
Published:
Migrated to https://github.com/BurtonQin/Awesome-Rust-Checker. Welcome to contribute there. Updated: 2024-11-21
Table of contents
Linters
| Name | Description | Working on | Bug types | Technology | Maintenance |
|---|---|---|---|---|---|
| clippy | A bunch of lints to catch common mistakes and improve your Rust code. Paper: ICSE-Companion’24 | HIR | Versatile | Pattern matching | ★★★★★ |
| dylint | Run Rust lints from dynamic libraries | HIR | Versatile | Pattern matching | ★★★★★ |
Static Checkers
| Name | Description | Working on | Bug Types | Technology | Maintenance |
|---|---|---|---|---|---|
| MIRAI | Rust mid-level IR Abstract Interpreter | MIR | Panic, Security bugs, Correctness | Abstract Interpretation | ★★★★★ |
| lockbud | Statically detect common memory and concurrrency bugs in Rust. Paper: Safety Issues in Rust, TSE’24 | MIR | Double-Lock, Conflicting-Lock-Order, Atomicity-Violation, Use-After-Free, Invalid-Free, Panic Locations | Data-flow Analysis | ★★★★★ |
| RAP (formerly SafeDrop) | Rust Analysis Platform. Paper: SafeDrop, TOSEM’22 | MIR | Use-After-Free, Double-Free | Data-flow Analysis | ★★★★★ |
| RCanary | Detecting Memory Leaks Across Semi-automated Memory Management Boundary in Rust. RCanary, TSE’24 | HIR, MIR | Memory Leaks | Static Program Analysis, Model Checking | ★★★☆☆ |
| Rudra | Rust Memory Safety & Undefined Behavior Detection. Paper: Rudra, SOSP’21 | HIR, MIR | Memory safety when panicked, Higher Order Invariant, Send Sync Variance | Data-flow Analysis | ★★★☆☆ |
| Yuga | Automatically Detecting Lifetime Annotation Bugs in the Rust Language. Paper: Yuga, ICSE’24 | HIR, MIR | Lifetime Annotation Bugs | Data-flow Analysis | ★★★★☆ |
| MirChecker | A Simple Static Analysis Tool for Rust. Paper: MirChecker, CCS’21 | MIR | Panic (including numerical), Lifetime Corruption (memory issues) | Abstract Interpretation | ★★☆☆☆ |
| FFIChecker | A Static Analysis Tool For Detecting Memory Management Bugs Between Rust and C/C++. Paper: FFIChecker, ESORICS’22 | LLVM IR | Memory issues across the Rust/C FFI | Abstract Interpretation | ★☆☆☆☆ |
| RUPTA | Supports pointer/alias analysis for Rust, operating on Rust MIR. It currently offers callsite-based pointer analysis. Paper: RUPTA, CC’24 | MIR | Not bugs, for callgraph construction | Callsite-based pointer analysis | ★★★★★ |
| Charon | Interface with the rustc compiler for the purpose of program verification. Paper: Charon | MIR, LLBC | An Analysis Framework for Rust | Convert MIR to LLBC for analysis | ★★★★★ |
| Cocoon | Static Information Flow Control in Rust. Paper: Cocoon, OOPSLA’24 | Rust Soure Code | Secrecy Leaks | Rust’s type system and procedural macros | ★★★★★ |
Academic Papers (source code not found yet)
| Name | Description | Working on | Bug Types | Technology |
|---|---|---|---|---|
| Rupair | Rupair: Towards Automatic Buffer Overflow Detection and Rectification for Rust. Rupair, ACSAC’21 | AST, MIR | Buffer Overflow | Data-flow Analysis |
| CRUST | CRUST: Towards a Unified Cross-Language Program Analysis Framework for Rust. CRUST, QRS’22 | CRustIR based on MIR | Security (CFI vilation, Meta Data Leaking, Format String Attack), Memory issues(Out-of-bounds, Use-after-Free, Double-Free, Stack-Overflow, Buffer-Overflow), Arithmetic (Divide-by-zero, Integer-Overflow) | Program Analysis Framework |
| ACORN | ACORN: Towards a Holistic Cross-Language Program Analysis for Rust. ACORN | Wasm | Security (Tainted Variable, Dangerous Function, Format String Attack), Memory issues (Out-of-bounds, Use-after-Free, Double-Free, Stack-Overflow, Buffer-Overflow), Arithmetic (Divide-by-zero, Integer-Overflow) | Program Analysis Framework |
| Yu Zhang | Static Deadlock Detection for Rust Programs. Yu Zhang | MIR | Deadlock | Data-flow Analysis |
| Kaiwen Zhang | Automatically Transform Rust Source to Petri Nets for Checking Deadlocks. Kaiwen Zhang | MIR | Deadlock | Petri Nets |
| RustC4 | Leveraging Large Language Model to Assist Detecting Rust Code Comment Inconsistency. ASE’24 | AST | Code Comment Inconsistency | LLM |
| craft | Automated Fault Tree Generation for Rust Programs. EDCC’24 | - | Fault Tree | Static Program Analysis |
| PanicFI | An Infrastructure for Fixing Panic Bugs in Real-World Rust Programs. PanicFI | HIR, AST | Fixing Panic Bugs | Pattern Matching |
Dynamic Checkers
| Name | Description | Working on | Bug Types | Technology | Maintenance |
|---|---|---|---|---|---|
| miri | An interpreter for Rust’s mid-level intermediate representation | MIR | Undefined Behavior | Abstract Interpretation | ★★★★★ |
| cargo-careful | Execute Rust code carefully, with extra checking along the way | - | Undefined Behavior | Enable Debug Assertion in std | ★★★★★ |
| cargo-fuzz | Command line helpers for fuzzing | - | - | Fuzzing | ★★★★★ |
| Loom | Concurrency permutation testing tool for Rust. | Source Code | Concurrency Bugs | Permutation testing | ★★★★★ |
| ERASAN | Efficient Rust Address Sanitizer. Paper: IEEES&P’24 | - | Memory Access Bugs | Fuzzing | ★★★★★ |
| Automated-Fuzzer | Simple tool to create broken files and checking them with special apps | - | Panic | Fuzzing | ★★★★★ |
| RULF | Fuzz Target Generator for Rust libraries. Paper: RULF, ASE’21 | - | Out-of-bound, Panic (including arithmetic) | Fuzzing | ★★★☆☆ |
| RPG1 | RPG: Rust Library Fuzzing with Pool-based Fuzz Target. Paper: RPG, ICSE’24 | - | Out-of-bound, Panic (including arithmetic) | Fuzzing | ★★☆☆☆ |
| SyRust | Automatic Testing of Rust Libraries with Semantic-Aware Program Synthesis. Paper: SyRust, PLDI’21 | - | - | Program Synthesis | ★☆☆☆☆ |
| NADER | Automatic Context-Aware Safety Enhancement for Rust. Paper: OOPSLA’21 | MIR, Source Code | Unchecked Indexing | API Replacing | ★☆☆☆☆ |
| casr2 | collect crash (or UndefinedBehaviorSanitizer error) reports, triage, and estimate severity. Paper: Casr-Cluster, ISPRAS’21, Ivannikov Memorial Workshop’24 | Crash Reports from ASan, UBSan, GDB | - | Analyze crashes | ★★★★★ |
| FRIES | Fuzzing Rust Library Interactions via Efficient Ecosystem-Guided Target Generation. Paper: FRIES, ISSTA’24 | MIR | Rust API interactions | Fuzzing | ★★★☆☆ |
| rustsmith | A randomized program fuzzer for the Rust programming language. Paper: rustsmith, ISSTA’23 rustsmith, thesis | AST | Rust compiler bugs | Differential testing | ★★★☆☆ |
| rustlantis | UB-free and deterministic rustc fuzzer. Paper: rustlantis, OOPSLA’24 | MIR | Rust compiler bugs | Differential testing | ★★★★★ |
Academic Papers (source code not found yet)
| Name | Description | Working on | Bug Types | Technology |
|---|---|---|---|---|
| CrabSandwich | CrabSandwich: Fuzzing Rust with Rust. CrabSandwich, Fuzzing’23 | LLVM IR | Out-of-bounds, Panic | Fuzzing |
| Zhiyong Ren | Detect Stack Overflow Bugs in Rust via Improved Fuzzing Technique. Zhiyong Ren, SEKE’21 | AST, HIR, MIR, LLVM IR | Stack Overflow | Fuzzing |
| Rustcheck | Safety Enhancement of Unsafe Rust via Dynamic Program Analysis. Rustcheck, QRS-C’23 | MIR | Memory vulnerabilities | Static Program Analysis, Instrumentation |
| RUSTY | A Fuzzing Tool for Rust. Poster@ACSAC’20 | - | Vulnerabilities | Fuzzing, Concolic Testing, Property-based Testing |
| Rust-twins | Automatic Rust Compiler Testing through Program Mutation and Dual Macros Generation. ASE’24 | AST, HIR | Rust compiler crashes and differences | Differential testing, mutation, macroize components, LLM |
| SafeFFI | Poster: Ensuring Memory Safety for the Transition from C/C++ to Rust. NDSS’24 | LLVM IR | Memory safety in C/C++ and Rust Mixed Code | Existing sanitiers: HWASAN, SoftBound/CETS |
- The link may be incorrect. See here.
- casr analyze the results of dynamic checkers instead of performing dynamic analysis itself. Thanks zjp-CN for recommending casr.
Verifiers
| Name | Description | Working on | Bug Types | Technology | Maintenance |
|---|---|---|---|---|---|
| kani | The Kani Rust Verifier is a bit-precise model checker for Rust. Paper: kani, ICSE-SEIP’22 | MIR | Memory safety, User-specified assertions, Panics, Unexpected behavior (e.g., arithmetic overflows) | Model Checking | ★★★★★ |
| prusti | A static verifier for Rust, based on the Viper verification infrastructure. Paper: prusti, NFM’22 | Viper | Panic (inluding arithmetic), User-specified assertions | Symbolic Execution | ★★★★☆ |
| crux-mir | A static simulator for Rust programs. Paper: crux | - | - | Symbolic Testing | ★★★★☆ |
| verus | Verified Rust for low-level systems code. Paper: verus, OOPSLA’23, SOSP’24 | - | - | SMT-based Verification5 | ★★★★★ |
| flux | flux is a refinement type checker for Rust. Paper: flux, PLDI’23 | - | - | - | ★★★★★ |
| Aeneas | A verification toolchain for Rust programs. Paper: Aeneas, ICFP’22, ICFP’24 | LLBC (for safe Rust only) | - | - | ★★★★★ |
| RustBelt | Formal (and machine-checked) safety proof for a language representing a realistic subset of Rust. Paper: RustBelt, POPL’18 | 𝜆Rust | - | - | ★★★★★ |
| RustHorn | A CHC-based automated verifier for Rust RustHorn, TOPLAS’21 | MIR | - | - | ★★★★☆ |
| Creusot | A deductive verifier for Rust code. Creusot, ICFEM’22 | WhyML | Panics, overflows, Assertion failures | Deductive Verification | ★★★★★ |
| RustHornBelt | A Semantic Foundation for Functional Verification of Rust Programs with Unsafe Code. Paper: RustHornBelt, PLDI’22 | 𝜆Rust | - | - | ★★☆☆☆ |
| RefinedRust1 | A Type System for High-Assurance Verification of Rust Programs. Paper: RefinedRust, PLDI’24 | Radium | - | - | ★★★★★ |
| VeriFast2 | Research prototype tool for modular formal verification of C and Java programs. Paper: VeriFast, NFM’11 | - | - | Symbolic Execution | ★★★★★ |
| mendel-verifier | Capability-based verifier for safe Rust clients of interior mutability. Paper: Poli, Thesis | Viper | Interior Mutability | Symbolic Execution | ★★★★★ |
| silver-sif-extension | Extension of the Viper language with modular product programs and information flow specifications. Paper: Thesis | Viper | Differential Privacy | Symbolic Execution | ★★★★★ |
Academic Papers (source code not found yet)
| Name | Description | Working on | Bug Types | Technology |
|---|---|---|---|---|
| GillianRust | A hybrid approach to semi-automated Rust verification. GillianRust | Unsafe Code Supported | - | Separation Logic based Hybrid Verification5 |
| UnsafeCop | Towards Memory Safety for Real-World Unsafe Rust Code with Practical Bounded Model checking. UnsafeCop, FM’24 | - | Memory safety issues | Bounded Model Checking |
| SAFE | Automated Proof Generation for Rust Code via Self-Evolution. SAFE | Rust Code With Docstring, Verus | - | Verus Verifier, LLM |
| PanicCheck | Broadly Enabling KLEE to Effortlessly Find Unrecoverable Errors. PanicCheck, ICSE-SEIP’24 | LLVM IR | Panic | KLEE |
- Thanks to jedbrown for recommending RefinedRust and other Rust-related verification tools.
- Rust support is WIP in VeriFast. Thanks zjp-CN for recommending VeriFast.
Thanks to the following awesome works:
- https://github.com/analysis-tools-dev/static-analysis?tab=readme-ov-file#rust
- https://github.com/analysis-tools-dev/dynamic-analysis?tab=readme-ov-file#rust
- A Survey of Rust Language Security Research
- RefinedRust: A Type System for High-Assurance Verification of Rust Programs
- Verifying the Rust Standard Library