model-checking
Tracking Issue: Automatically Verify Memory Initialization
Goal: Implement automated and efficient checks for memory initialization in Kani.
Motivation
Safe Rust guarantees that every variable is initialized, and every reference points to a properly allocated and initialized memory position. The same guarantees do not apply to raw pointers, transmute operations and unions, which are available in unsafe Rust. The safe usage of these constructs and operations must be upheld by the Rust developer.
Failures to uphold these safety properties can have unwanted consequences: it can affect the application behavior and even result in the application exposing critical data.
Kani should be able to detect uninitialized memory accesses automatically and efficiently.
Examples
Currently, Kani does not catch the following cases of UB due to accessing uninitialized memory:
#[repr(C)]
struct S(u32, u8);
#[kani::proof]
fn check_uninit_padding() {
let s = S(0, 0);
let ptr: *const u8 = addr_of!(s) as *const u8;
let padding = unsafe { *(ptr.add(5)) }; // ~ERROR: padding bytes are uninitialized, so reading them is UB.
}
#[kani::proof]
fn check_vec_read_uninit() {
let v: Vec<u8> = Vec::with_capacity(10);
let uninit = unsafe { *v.as_ptr().add(5) }; // ~ERROR: reading from unitialized memory is UB.
}
Tasks
- [x] Implement brute-force memory initialization checks for raw pointers (#3264)
- [x] Make sure layout representation does not negatively affect performance (#3313)
- [x] Fix behavior of
copyandcopy_nonoverlapping(#3347, #3350) - [x] Add support for delayed UB via static analysis (#3324, #3374)
- [x] Handle intrinsics systematically (#3422)
- [ ] Add support for vtable and function pointer calls
- [ ] Add support for recursive function analysis
- [ ] Add support for
enums with variants that have different padding - [ ] Add support for
unions (#896)- [x] Unions can be created, assigned to, read from (#3444)
- [x] Unions can be passed as arguments to other functions (#3465)
- [ ] Unions can serve as a pointee of raw pointers, a field of structs / unions
- [ ] Add support for
extern statics - [ ] Add support for trait objects
// ~ERROR: padding bytes are uninitialized, so reading them is UB.
The Rust reference mentions that reading padding bytes is not UB:
In other words, the only cases in which reading uninitialized memory is permitted are inside unions and in "padding" (the gaps between the fields/elements of a type).
@zhassan-aws thanks for pointing that out -- I interpret the Rust reference a bit differently in this case.
I take the words you quoted to mean that it is indeed not UB to read padding bytes and treat them as padding bytes. I.e. reading a mix of data bytes and padding bytes and then storing it in a struct with an appropriate layout is not UB. However, the example above reads padding bytes into the type without valid value restrictions, which should be UB.
I see. Can you post the full example (e.g. the definition of S)? We can check what MIRI says.
Updated the example above, sorry for that!
Here is the output from MIRI:
error: Undefined Behavior: using uninitialized data, but this operation requires initialized memory
--> src/main.rs:9:28
|
9 | let padding = unsafe { *(ptr.add(5)) }; // ~ERROR: padding bytes are uninitialized, so reading them is UB.
| ^^^^^^^^^^^^^ using uninitialized data, but this operation requires initialized memory
|
= help: this indicates a bug in the program: it performed an invalid operation, and caused Undefined Behavior
= help: see https://doc.rust-lang.org/nightly/reference/behavior-considered-undefined.html for further information
= note: BACKTRACE:
= note: inside `main` at src/main.rs:9:28: 9:41