Page Not Found
Page not found. Your pixels are in another canvas.
Sitemap
A list of all the posts and pages found on the site. For you robots out there is an XML version available for digesting as well.
Pages
Boqin Qin's Website
About me
Page not in menu
This is a page not in th emain menu
Posts
A curated list of awesome Rust checkers
Published:
Migrated to https://github.com/BurtonQin/Awesome-Rust-Checker. Welcome to contribute there. Updated: 2024-11-18
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 |
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 |
- 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 | ★★★★★ |
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 |
- 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
A Use-After-Free Bug in Redox
Published:
This is the brief description of CVE-2020-22429. For more details, please refer to Reference.
portfolio
Portfolio
This is me!
publications
An Adaptive Encryption-as-a-Service Architecture Based on Fog Computing for Real-Time Substation Communications
Published in IEEE Transactions on Industrial Informatics, 16(1), 658-668, 2019
We present a novel encryption-as-a-service architecture based on fog computing.
Recommended citation: Zhang, H., Qin, B., Tu, T., Guo, Z., Gao, F., & Wen, Q. (2019). An adaptive encryption-as-a-service architecture based on fog computing for real-time substation communications. IEEE Transactions on Industrial Informatics, 16(1), 658-668. https://doi.org/10.1109/TII.2019.2948113
Understanding memory and thread safety practices and issues in real-world Rust programs
Published in PLDI 2020: Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and ImplementationJune 2020 Pages 763–779, 2020
Our study reveals interesting real-world Rust program behaviors and new issues Rust programmers make.
Recommended citation: Qin, B., Chen, Y., Yu, Z., Song, L., & Zhang, Y. (2020, June). Understanding memory and thread safety practices and issues in real-world Rust programs. In Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation (pp. 763-779). https://doi.org/10.1145/3385412.3386036
Measuring and Modeling the Label Dynamics of Online Anti-Malware Engines
Published in USENIX Security 2020: 29th USENIX Security Symposium Pages 2361-2378, 2020
We take a data-driven approach to categorize, reason, and validate common labeling methods used by researchers.
Recommended citation: Zhu, S., Shi, J., Yang, L., Qin, B., Wang, G., & Song, L. (2020, August). Measuring and Modeling the Label Dynamics of Online Anti-Malware Engines. 29th USENIX Security Symposium (pp. 2361-2378). https://www.usenix.org/conference/usenixsecurity20/presentation/zhu
Demo: VRLifeTime – An IDE Tool to Avoid Concurrency and Memory Bugs in Rust
Published in Demo@CCS 2020: Proceedings of the 2020 ACM SIGSAC Conference on Computer and Communications Security Pages 2085–2087, 2020
We present VRLifeTime, an IDE tool that can visualize lifetime for Rust programs and help programmers avoid lifetime-related mistakes.
Recommended citation: Zhang, Z., Qin, B., Chen, Y., Song, L., & Zhang, Y. (2020, November). VRLifeTime -- An IDE Tool to Avoid Concurrency and Memory Bugs in Rust. In Proceedings of the 2020 ACM SIGSAC Conference on Computer and Communications Security Pages (pp. 2085–2087). https://dl.acm.org/doi/10.1145/3372297.3420024
Algorithmic Profiling for Real-World Complexity Problems
Published in IEEE Transactions on Software Engineering, Early Access, 2021
We design a tool, ComAir, which can effectively conduct algorithmic profiling in production environment.
Recommended citation: Qin, B., Tu, T., Liu, Z., Yu, T., & Song, L. (2021). Algorithmic Profiling for Real-World Complexity Problems. IEEE Transactions on Software Engineering. https://doi.org/10.1109/TSE.2021.3067652
Automatically Detecting and Fixing Concurrency Bugs in Go Software Systems
Published in ASPLOS 2021: Proceedings of the 26th ACM International Conference on Architectural Support for Programming Languages and Operating Systems 2021 Pages 616–629, 2021
This paper proposes static concurrency bug detection system, GCatch, and an automated concurrency bug fixing system, GFix.
Recommended citation: Liu, Z., Zhu, S., Qin, B., Chen, H., & Song, L. (2021, April). Automatically detecting and fixing concurrency bugs in go software systems. In Proceedings of the 26th ACM International Conference on Architectural Support for Programming Languages and Operating Systems (pp. 616–629). https://doi.org/10.1145/3445814.3446756
Learning and Programming Challenges of Rust: A Mixed-Methods Study
Published in ICSE 2022: Proceedings of the 2022 International Conference on Software Engineering, 2022
Survey Rust programmers for the challenges of learning and programming Rust
Recommended citation: Zhu, S., Zhang, Z., Qin, B., Xiong, A., & Song, L. (2022, May). Learning and Programming Challenges of Rust: A Mixed-Methods Study. In Proceedings of the 44th International Conference on Software Engineering. https://doi.org/10.1145/3510003.3510164
Understanding and Detecting Real-World Safety Issues in Rust
Published in IEEE Transactions on Software Engineering, 2024
Our study reveals interesting real-world Rust program behaviors and new issues Rust programmers make.
Recommended citation: Qin, B., Chen, Y., Liu, H., Zhang, H., Wen, Q., Song, L., & Zhang, Y. (2024). IEEE Transactions on Software Engineering. https://songlh.github.io/paper/rust-tse.pdf
talks
Algorithmic Profiling for Real-World Complexity Problems
Published:
My Journal-First paper in ICSE’22. https://www.youtube.com/watch?v=M1hfaHPB868