XRust:检测 Rust Linux 驱动中的逻辑竞态
原标题:XRust: Detecting Logical Races in Rust Linux Drivers
AI 摘要
该论文提出 XRust,一种无需人工编写不变量即可检测 Linux Rust 驱动中逻辑竞态的技术。它基于 Logical Happens-Before 分析识别与逻辑顺序相关的共享状态访问,自动构造操作对测试框架,并用串行差分判定器检测与任一串行顺序不一致的并发执行。在 Linux 7.3-rc2 上,XRust 覆盖 10 个驱动的 102 个 Rust 文件,构造 1,654 个可执行测试框架,发现两个此前未知的逻辑竞态,其中 rnull 块驱动的竞态已被 Linux 维护者确认并合入修复。
正文节选
XRust: Detecting Logical Races in Rust Linux Drivers Abstract. Rust is increasingly used in Linux to improve memory safety, but its guarantees do not prevent logical races: individually synchronized operations can still interleave in ways that violate higher-level invariants. Detecting such bugs typically requires manually written specifications and carefully controlled execution environments. We present XRust, a technique for detecting logical races in Linux Rust drivers without manually specif