Posts by Tags

Ads

招生广告

less than 1 minute read

Published:

中国科学院计算技术研究所处理器芯片全国重点实验室宋林海老师课题组招收硕士生、直博生

CVE

Recruiting

招生广告

less than 1 minute read

Published:

中国科学院计算技术研究所处理器芯片全国重点实验室宋林海老师课题组招收硕士生、直博生

Redox

Rust

A curated list of awesome Rust checkers

5 minute read

Published:

Migrated to https://github.com/BurtonQin/Awesome-Rust-Checker. Welcome to contribute there.

Table of contents

Linters

NameDescriptionWorking onBug typesTechnologyMaintenance
clippyA bunch of lints to catch common mistakes and improve your Rust code.HIRVersatilePattern matching★★★★★
dylintRun Rust lints from dynamic librariesHIRVersatilePattern matching★★★★★

Static Checkers

NameDescriptionWorking onBug TypesTechnologyMaintenance
MIRAIRust mid-level IR Abstract InterpreterMIRPanic, Security bugs, CorrectnessAbstract Interpretation★★★★★
lockbudStatically detect common memory and concurrrency bugs in Rust. Paper: Safety Issues in Rust, TSE’24MIRDouble-Lock, Conflicting-Lock-Order, Atomicity-Violation, Use-After-Free, Invalid-Free, Panic LocationsData-flow Analysis★★★★★
RAP (formerly SafeDrop)Rust Analysis Platform. Paper: SafeDrop, TOSEM’22MIRUse-After-Free, Double-FreeData-flow Analysis★★★★★
RudraRust Memory Safety & Undefined Behavior Detection. Paper: Rudra, SOSP’21HIR, MIRMemory safety when panicked, Higher Order Invariant, Send Sync VarianceData-flow Analysis★★★☆☆
YugaAutomatically Detecting Lifetime Annotation Bugs in the Rust Language. Paper: Yuga, ICSE’24HIR, MIRLifetime Annotation BugsData-flow Analysis★★★★☆
MirCheckerA Simple Static Analysis Tool for Rust. Paper: MirChecker, CCS’21MIRPanic (including numerical), Lifetime Corruption (memory issues)Abstract Interpretation★★☆☆☆
FFICheckerA Static Analysis Tool For Detecting Memory Management Bugs Between Rust and C/C++. Paper: FFIChecker, ESORICS’22LLVM IRMemory issues across the Rust/C FFIAbstract Interpretation★☆☆☆☆

Academic Papers (source code not found yet)

NameDescriptionWorking onBug TypesTechnology
RupairRupair: Towards Automatic Buffer Overflow Detection and Rectification for Rust. Rupair, ACSAC’21AST, MIRBuffer OverflowData-flow Analysis
RCanaryrCanary: Detecting Memory Leaks Across Semi-automated Memory Management Boundary in Rust. RCanaryHIR, MIRMemory LeaksStatic Program Analysis, Model Checking
CRUSTCRUST: Towards a Unified Cross-Language Program Analysis Framework for Rust. CRUST, QRS’22CRustIR based on MIRSecurity (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
ACORNACORN: Towards a Holistic Cross-Language Program Analysis for Rust. ACORNWasmSecurity (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 ZhangStatic Deadlock Detection for Rust Programs. Yu ZhangMIRDeadlockData-flow Analysis
Kaiwen ZhangAutomatically Transform Rust Source to Petri Nets for Checking Deadlocks. Kaiwen ZhangMIRDeadlockPetri Nets

Dynamic Checkers

NameDescriptionWorking onBug TypesTechnologyMaintenance
miriAn interpreter for Rust’s mid-level intermediate representationMIRUndefined BehaviorAbstract Interpretation★★★★★
cargo-carefulExecute Rust code carefully, with extra checking along the way-Undefined BehaviorEnable Debug Assertion in std★★★★★
cargo-fuzzCommand line helpers for fuzzing--Fuzzing★★★★★
LoomConcurrency permutation testing tool for Rust.Source CodeConcurrency BugsPermutation testing★★★★★
ERASANEfficient Rust Address Sanitizer. Paper: IEEES&P’24-Memory Access BugsFuzzing★★★★★
Automated-FuzzerSimple tool to create broken files and checking them with special apps-PanicFuzzing★★★★★
RULFFuzz Target Generator for Rust libraries. Paper: RULF, ASE’21-Out-of-bound, Panic (including arithmetic)Fuzzing★★★☆☆
RPG1RPG: Rust Library Fuzzing with Pool-based Fuzz Target. Paper: RPG, ICSE’24-Out-of-bound, Panic (including arithmetic)Fuzzing★★☆☆☆
SyRustAutomatic Testing of Rust Libraries with Semantic-Aware Program Synthesis. Paper: SyRust, PLDI’21--Program Synthesis★☆☆☆☆
NADERAutomatic Context-Aware Safety Enhancement for Rust. Paper: OOPSLA’21MIR, Source CodeUnchecked IndexingAPI Replacing★☆☆☆☆
casr2collect crash (or UndefinedBehaviorSanitizer error) reports, triage, and estimate severity. Paper: Casr-Cluster, ISPRAS’21, Ivannikov Memorial Workshop’24Crash Reports from ASan, UBSan, GDB-Analyze crashes★★★★★

Academic Papers (source code not found yet)

NameDescriptionWorking onBug TypesTechnology
CrabSandwichCrabSandwich: Fuzzing Rust with Rust. CrabSandwich, Fuzzing’23LLVM IROut-of-bounds, PanicFuzzing
Zhiyong RenDetect Stack Overflow Bugs in Rust via Improved Fuzzing Technique. Zhiyong Ren, SEKE’21AST, HIR, MIR, LLVM IRStack OverflowFuzzing
RustheckSafety Enhancement of Unsafe Rust via Dynamic Program Analysis. Rustcheck, QRS-C’23MIRMemory vulnerabilitiesStatic Program Analysis, Instrumentation
  1. The link may be incorrect. See here.
  2. casr analyze the results of dynamic checkers instead of performing dynamic analysis itself. Thanks zjp-CN for recommending casr.

Verifiers1

NameDescriptionWorking onBug TypesTechnologyMaintenance
kaniThe Kani Rust Verifier is a bit-precise model checker for Rust. Paper: kani, ICSE-SEIP’22MIRMemory safety, User-specified assertions, Panics, Unexpected behavior (e.g., arithmetic overflows)Model Checking★★★★★
prustiA static verifier for Rust, based on the Viper verification infrastructure. Paper: prusti, NFM’22 ViperPanic (inluding arithmetic), User-specified assertionsSymbolic Execution★★★★☆
crux-mirA static simulator for Rust programs--Symbolic Testing★★★★☆
verusVerified Rust for low-level systems code. Paper: verus, OOPSLA’23---★★★★★
fluxflux is a refinement type checker for Rust. Paper: flux, PLDI’23---★★★★★
AeneasA verification toolchain for Rust programs. Paper: Aeneas, ICFP’22LLBC (for safe Rust only)--★★★★★
RustBeltFormal (and machine-checked) safety proof for a language representing a realistic subset of Rust. Paper: RustBelt, POPL’18𝜆Rust--★★★★★
RustHornA CHC-based automated verifier for Rust RustHorn, TOPLAS’21MIR--★★★★☆
CreusotA deductive verifier for Rust code. Creusot, ICFEM’22WhyMLPanics, overflows, Assertion failures-★★★★★
RustHornBeltA Semantic Foundation for Functional Verification of Rust Programs with Unsafe Code. Paper: RustHornBelt, PLDI’22𝜆Rust--★★☆☆☆
RefinedRustA Type System for High-Assurance Verification of Rust Programs. Paper: RefinedRust, PLDI’24Radium--★★★★★

Academic Papers (source code not found yet)

NameDescriptionWorking onBug TypesTechnology
GillianRustA hybrid approach to semi-automated Rust verification. GillianRust---
  1. Thanks to jedbrown for recommending RefinedRust and other Rust-related verification tools.

Thanks to the following awesome works:

  1. https://github.com/analysis-tools-dev/static-analysis?tab=readme-ov-file#rust
  2. https://github.com/analysis-tools-dev/dynamic-analysis?tab=readme-ov-file#rust
  3. A Survey of Rust Language Security Research
  4. RefinedRust: A Type System for High-Assurance Verification of Rust Programs

Rust checkers

A curated list of awesome Rust checkers

5 minute read

Published:

Migrated to https://github.com/BurtonQin/Awesome-Rust-Checker. Welcome to contribute there.

Table of contents

Linters

NameDescriptionWorking onBug typesTechnologyMaintenance
clippyA bunch of lints to catch common mistakes and improve your Rust code.HIRVersatilePattern matching★★★★★
dylintRun Rust lints from dynamic librariesHIRVersatilePattern matching★★★★★

Static Checkers

NameDescriptionWorking onBug TypesTechnologyMaintenance
MIRAIRust mid-level IR Abstract InterpreterMIRPanic, Security bugs, CorrectnessAbstract Interpretation★★★★★
lockbudStatically detect common memory and concurrrency bugs in Rust. Paper: Safety Issues in Rust, TSE’24MIRDouble-Lock, Conflicting-Lock-Order, Atomicity-Violation, Use-After-Free, Invalid-Free, Panic LocationsData-flow Analysis★★★★★
RAP (formerly SafeDrop)Rust Analysis Platform. Paper: SafeDrop, TOSEM’22MIRUse-After-Free, Double-FreeData-flow Analysis★★★★★
RudraRust Memory Safety & Undefined Behavior Detection. Paper: Rudra, SOSP’21HIR, MIRMemory safety when panicked, Higher Order Invariant, Send Sync VarianceData-flow Analysis★★★☆☆
YugaAutomatically Detecting Lifetime Annotation Bugs in the Rust Language. Paper: Yuga, ICSE’24HIR, MIRLifetime Annotation BugsData-flow Analysis★★★★☆
MirCheckerA Simple Static Analysis Tool for Rust. Paper: MirChecker, CCS’21MIRPanic (including numerical), Lifetime Corruption (memory issues)Abstract Interpretation★★☆☆☆
FFICheckerA Static Analysis Tool For Detecting Memory Management Bugs Between Rust and C/C++. Paper: FFIChecker, ESORICS’22LLVM IRMemory issues across the Rust/C FFIAbstract Interpretation★☆☆☆☆

Academic Papers (source code not found yet)

NameDescriptionWorking onBug TypesTechnology
RupairRupair: Towards Automatic Buffer Overflow Detection and Rectification for Rust. Rupair, ACSAC’21AST, MIRBuffer OverflowData-flow Analysis
RCanaryrCanary: Detecting Memory Leaks Across Semi-automated Memory Management Boundary in Rust. RCanaryHIR, MIRMemory LeaksStatic Program Analysis, Model Checking
CRUSTCRUST: Towards a Unified Cross-Language Program Analysis Framework for Rust. CRUST, QRS’22CRustIR based on MIRSecurity (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
ACORNACORN: Towards a Holistic Cross-Language Program Analysis for Rust. ACORNWasmSecurity (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 ZhangStatic Deadlock Detection for Rust Programs. Yu ZhangMIRDeadlockData-flow Analysis
Kaiwen ZhangAutomatically Transform Rust Source to Petri Nets for Checking Deadlocks. Kaiwen ZhangMIRDeadlockPetri Nets

Dynamic Checkers

NameDescriptionWorking onBug TypesTechnologyMaintenance
miriAn interpreter for Rust’s mid-level intermediate representationMIRUndefined BehaviorAbstract Interpretation★★★★★
cargo-carefulExecute Rust code carefully, with extra checking along the way-Undefined BehaviorEnable Debug Assertion in std★★★★★
cargo-fuzzCommand line helpers for fuzzing--Fuzzing★★★★★
LoomConcurrency permutation testing tool for Rust.Source CodeConcurrency BugsPermutation testing★★★★★
ERASANEfficient Rust Address Sanitizer. Paper: IEEES&P’24-Memory Access BugsFuzzing★★★★★
Automated-FuzzerSimple tool to create broken files and checking them with special apps-PanicFuzzing★★★★★
RULFFuzz Target Generator for Rust libraries. Paper: RULF, ASE’21-Out-of-bound, Panic (including arithmetic)Fuzzing★★★☆☆
RPG1RPG: Rust Library Fuzzing with Pool-based Fuzz Target. Paper: RPG, ICSE’24-Out-of-bound, Panic (including arithmetic)Fuzzing★★☆☆☆
SyRustAutomatic Testing of Rust Libraries with Semantic-Aware Program Synthesis. Paper: SyRust, PLDI’21--Program Synthesis★☆☆☆☆
NADERAutomatic Context-Aware Safety Enhancement for Rust. Paper: OOPSLA’21MIR, Source CodeUnchecked IndexingAPI Replacing★☆☆☆☆
casr2collect crash (or UndefinedBehaviorSanitizer error) reports, triage, and estimate severity. Paper: Casr-Cluster, ISPRAS’21, Ivannikov Memorial Workshop’24Crash Reports from ASan, UBSan, GDB-Analyze crashes★★★★★

Academic Papers (source code not found yet)

NameDescriptionWorking onBug TypesTechnology
CrabSandwichCrabSandwich: Fuzzing Rust with Rust. CrabSandwich, Fuzzing’23LLVM IROut-of-bounds, PanicFuzzing
Zhiyong RenDetect Stack Overflow Bugs in Rust via Improved Fuzzing Technique. Zhiyong Ren, SEKE’21AST, HIR, MIR, LLVM IRStack OverflowFuzzing
RustheckSafety Enhancement of Unsafe Rust via Dynamic Program Analysis. Rustcheck, QRS-C’23MIRMemory vulnerabilitiesStatic Program Analysis, Instrumentation
  1. The link may be incorrect. See here.
  2. casr analyze the results of dynamic checkers instead of performing dynamic analysis itself. Thanks zjp-CN for recommending casr.

Verifiers1

NameDescriptionWorking onBug TypesTechnologyMaintenance
kaniThe Kani Rust Verifier is a bit-precise model checker for Rust. Paper: kani, ICSE-SEIP’22MIRMemory safety, User-specified assertions, Panics, Unexpected behavior (e.g., arithmetic overflows)Model Checking★★★★★
prustiA static verifier for Rust, based on the Viper verification infrastructure. Paper: prusti, NFM’22 ViperPanic (inluding arithmetic), User-specified assertionsSymbolic Execution★★★★☆
crux-mirA static simulator for Rust programs--Symbolic Testing★★★★☆
verusVerified Rust for low-level systems code. Paper: verus, OOPSLA’23---★★★★★
fluxflux is a refinement type checker for Rust. Paper: flux, PLDI’23---★★★★★
AeneasA verification toolchain for Rust programs. Paper: Aeneas, ICFP’22LLBC (for safe Rust only)--★★★★★
RustBeltFormal (and machine-checked) safety proof for a language representing a realistic subset of Rust. Paper: RustBelt, POPL’18𝜆Rust--★★★★★
RustHornA CHC-based automated verifier for Rust RustHorn, TOPLAS’21MIR--★★★★☆
CreusotA deductive verifier for Rust code. Creusot, ICFEM’22WhyMLPanics, overflows, Assertion failures-★★★★★
RustHornBeltA Semantic Foundation for Functional Verification of Rust Programs with Unsafe Code. Paper: RustHornBelt, PLDI’22𝜆Rust--★★☆☆☆
RefinedRustA Type System for High-Assurance Verification of Rust Programs. Paper: RefinedRust, PLDI’24Radium--★★★★★

Academic Papers (source code not found yet)

NameDescriptionWorking onBug TypesTechnology
GillianRustA hybrid approach to semi-automated Rust verification. GillianRust---
  1. Thanks to jedbrown for recommending RefinedRust and other Rust-related verification tools.

Thanks to the following awesome works:

  1. https://github.com/analysis-tools-dev/static-analysis?tab=readme-ov-file#rust
  2. https://github.com/analysis-tools-dev/dynamic-analysis?tab=readme-ov-file#rust
  3. A Survey of Rust Language Security Research
  4. RefinedRust: A Type System for High-Assurance Verification of Rust Programs

Use-after-free