一句话:提出 Miri,首个能发现确定性 Rust 程序中全部事实性未定义行为的动态检测工具。
Rust 一方面通过强类型系统保证内存与线程安全,另一方面在编译器无法静态保证安全属性时仍大量依赖 unsafe 代码。编写 unsafe Rust 的难度堪比 C/C++:一处错误即可引入未定义行为(UB),使程序脱离语言抽象机描述、以任意方式出错,常导致安全问题。本文提出 Miri,这是首个能够发现确定性 Rust 程序中所有事实性 UB 的工具。其关键特性包括指针 provenance 追踪、Rust 类型不变量校验、数据竞争检测、弱内存行为探索,以及实现足够的基础 OS API(如文件系统访问与并发原语),从而可直接运行未修改的真实 Rust 代码。作者在超过 10 万个 Rust 库上评估,成功执行了其合并测试套件中 70% 以上的测试;Miri 已发现数十个真实缺陷,并集成进 Rust 标准库及众多知名库的 CI,持续阻止更多缺陷进入代码库。
The Rust programming language has two faces: on the one hand, it is a high-level language with a strong type system ensuring memory and thread safety. On the other hand, Rust crucially relies on unsafe code for cases where the compiler is unable to statically ensure basic safety properties. The challenges of writing unsafe Rust are similar to those of writing C or C++: a single mistake in the program can lead to Undefined Behavior , which means the program is no longer described by the language's Abstract Machine and can go wrong in arbitrary ways, often causing security issues. Ensuring the absence of Undefined Behavior bugs is therefore a high priority for unsafe Rust authors. In this paper we present Miri , the first tool that can find all de-facto Undefined Behavior in deterministic Rust programs. Some of the key non-trivial features of Miri include tracking of pointer provenance, validation of Rust type invariants, data-race detection, exploration of weak memory behaviors, and implementing enough basic OS APIs (such as file system access and concurrency primitives) to be able to run unchanged real-world Rust code. In an evaluation on more than 100 000 Rust libraries, Miri was able to successfully execute more than 70% of the tests across their combined test suites. Miri has found dozens of real-world bugs and has been integrated into the continuous integration of the Rust standard library and many prominent Rust libraries, preventing many more bugs from ever entering these codebases.
@article{JungKPMSW26,
title = {Miri: Practical Undefined Behavior Detection for Rust},
author = {Ralf Jung and Benjamin Kimock and Christian Poveda and Eduardo Sánchez Muñoz and Oli Scherer and Qian Wang},
journal = {Proceedings of the ACM on Programming Languages},
volume = {10},
number = {POPL},
year = {2026},
doi = {10.1145/3776690}
}