Miri: Practical Undefined Behavior Detection for Rust
summary
Miri is an interpreter of Rust’s abstract machine that tracks per-byte initialization and pointer provenance, enforces Rust type representations, detects data races via vector‑clock-style checking, and emulates weak memory behaviors plus enough OS APIs to run real crates unchanged. The paper claims Miri can find all de‑facto UB in deterministic Rust; it successfully executes 70% of tests across ~100,000 crates, finds dozens of real bugs and integrates into CI, while running ~10^4–10^5× slower and not calling native C.
AI-written summary · about
chapters (17)
- 0:00Miri introduction
- 1:02Safe vs unsafe Rust
- 3:30Undefined behavior consequences
- 5:18How Miri detects UB
- 7:23Miri’s abstract machine
- 9:52Type encoding in Miri
- 10:54Detecting data races
- 12:39Weak memory behaviors
- 14:25Miri’s limitations
- 16:32Miri’s real-world impact
- 17:35Evaluating Miri on crates
- 18:40Future work for Miri
- 19:23Conclusion
- 19:44Q&A: Miri’s completeness
- 20:47Q&A: Address space nondeterminism
- 21:29Q&A: Formalizing UB in Rust
- 22:54Q&A: Miri for other languages
related talks
44mMiri, Undefined Behavior and Foreign Functions
59mWhat's the deal with unsafe Rust?
21mMind the Boundary: Detecting Undefined Behavior Across Rust’s FFI
58mRust for The Curious C++ Developers
40mBorrowSanitizer: Securing Rust Across Foreign Function Boundaries
34mMiniRust: A core language for specifying Rust
15mHow Do Programmers Use Unsafe Rust?
14mAn Empirical Study of Bugs in the rustc Compiler