Klint: Compile-time Detection of Atomic Context Violations for Kernel Rust Code
summary
Klint is a compile-time checker for Kernel Rust that enforces compile-time detection of sleeping-in-atomic-context errors by tracking a function’s relative preemption-count adjustment and its expected entry range. It infers properties for most Rust code, requires explicit annotations at FFI and ArcWake boundaries, and already found a real RCU-related UAF bug where a waker kept a task alive and dropped it inside atomic context. Current limits: conditional/data-dependent lock paths, function-pointer calls, and Rust-generated extra drops.
AI-written summary · about
chapters (10)
- 0:00Introduction and context
- 1:26Introducing Pink tool
- 2:08Rust safety and atomic context
- 7:27Safety requirements for APIs
- 11:45Design goals of Pink
- 13:54How Pink enforces rules
- 16:05Annotating functions in Pink
- 19:16Case study on Linux kernel
- 23:13Limitations and future work
- 26:00Conclusion and resources
related talks
15mSafer at Any Speed: Automatic Context-Aware Safety Enhancement for Rust
32mBuilding and Maintaining Rust at Scale
31mValidating Rust for industry: Certification meets formal analysis
25m"Compiler-Driven Development: Making Rust Work for You"
19mCounterexamples in Safe Rust
30mOverflowing with Fear: Detecting and Mitigating Implicit Panics in Rust
39mRust Atomics in the Wild: Memory Ordering Design Patterns [...]
45mBuilding Safe and Secure Systems in Rust