A curated list of awesome Rust checkers
July 13, 2024
Awesome Rust checkers Migrated to https://github.com/BurtonQin/Awesome-Rust-Checker . Welcome to contribute there.
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. 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 ★★★★★ 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 ★☆☆☆☆
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 RCanary rCanary: Detecting Memory Leaks Across Semi-automated Memory Management Boundary in Rust. RCanary HIR, MIR Memory Leaks Static Program Analysis, Model Checking 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
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 ★★★☆☆ RPG 1 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 ★☆☆☆☆
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 Rustheck Safety Enhancement of Unsafe Rust via Dynamic Program Analysis. Rustcheck, QRS-C’23 MIR Memory vulnerabilities Static Program Analysis, Instrumentation
The link may be incorrect. See here . Verifiers1 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 - - Symbolic Testing ★★★★☆ verus Verified Rust for low-level systems code. Paper: verus, OOPSLA’23 - - - ★★★★★ flux flux is a refinement type checker for Rust. Paper: flux, PLDI’23 - - - ★★★★★ Aeneas A verification toolchain for Rust programs. Paper: Aeneas, ICFP’22 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 - ★★★★★ RustHornBelt A Semantic Foundation for Functional Verification of Rust Programs with Unsafe Code. Paper: RustHornBelt, PLDI’22 𝜆Rust - - ★★☆☆☆ RefinedRust A Type System for High-Assurance Verification of Rust Programs. Paper: RefinedRust, PLDI’24 Radium - - ★★★★★
Academic Papers (source code not found yet)
Name Description Working on Bug Types Technology GillianRust A hybrid approach to semi-automated Rust verification. GillianRust - - -
Thanks to jedbrown for recommending RefinedRust and other Rust-related verification tools. 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 