Symbolic Testing for Rust with crux-mir

Explore symbolic testing for Rust with crux-mir in this 42-minute conference talk presented by Aaron Tomb and Stuart Pernsteiner. Dive into the general features, targets, and design architecture of crux-mir, including its use of the Crucible language and symbolic execution strategy. Examine how crux-mir handles Rust's memory model, generics, iterator adapters, and monomorphization. Learn about the tool's approach to unsafe code, raw pointers, transmute and integer casts, low-level pointer offsets, and the slice library. Discover the Cargo integration and future work planned for crux-mir. The talk concludes with a Q&A session covering topics such as model organization, dynamic symbolic execution, multiple shared references, and handling of string and C intrinsics.

Intro
What is cruxmir
General features
Targets
Scalar 52 example
Design architecture
Crucible language
Symbolic execution strategy
Rust memory model
Generics
Iterator adapters
Monomorphization
Peekaboo
Monomorphizing
Recap
Unsafe code
Raw pointers
Transmute and integer casts
Lowlevel pointer offset
Slice library
Deallocate
Cargo integration
Future work
Questions
Model organization
Dynamic symbolic execution
No concolic execution
Multiple shared references
Export mirror
Cargo mirror wrapper
String intrinsics
C intrinsics
C long tail