Scalable Bug Detection for Internally Unsafe Libraries: A Logical Approach to Type(…)
summary
Claims a fully automatic under-approximate method that refutes type soundness in libraries by encoding type assignments as separation-logic assertions and using incorrectness separation logic plus symbolic execution over inferred type spaces. Prototype implements the algorithm for a simplified lambda-Rust and demonstrates finding real memory-safety bugs with no false positives though bounded exploration causes false negatives. Current limitations: no references support yet (so misses iterator-invalidation style bugs) and a Coq-style formalization accompanies the work.
AI-written summary · about
chapters (12)
- 0:00Safe vs unsafe Rust abstractions
- 1:44Rust’s type system for memory safety
- 3:54C’s lack of type safety
- 5:22Type/soundness issues in Rust
- 7:10Rux for automatic bug detection
- 12:56Demo: Rux on even numbers
- 14:21Symbolic execution on types
- 15:03Q&A: Library boundaries
- 15:24Q&A: Combining libraries
- 16:08Q&A: Standard library integration
- 16:52Q&A: RustBelt comparison
- 17:59Closing remarks
related talks
21mMind the Boundary: Detecting Undefined Behavior Across Rust’s FFI
28mDetecting Borrow and Provenance Bugs Across Unsafe Rust [...]
32mSafer Code with LLMs: Scala Types Silver Bullet?
53mLightweight Resource Leak Verification and Inference
01h 00mAI Safety through Programming?
35m"Memory Safety is Merely Table Stakes [...]"
25mTowards Understanding Spectre-PHT in Memory-Safe Languages
01h 01mClosing the Gap between Rust and C++ Using Principles of Static Analysis