Tracking Issue: Automatically Verify Memory Initialization

artemagvanian commented 3 days ago

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

[ ] Implement brute-force memory initialization checks for raw pointers (#3264)
[ ] Make sure layout representation does not negatively affect performance
[ ] Implement pruning unnecessary checks via static analysis
[ ] Add support for enums with variants that have different padding
[ ] Add support for transmutes
[ ] Add support for unions
[ ] Add support for extern statics
[ ] https://github.com/model-checking/kani/issues/896

zhassan-aws commented 2 days ago

// ~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).

artemagvanian commented 2 days ago

@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.

zhassan-aws commented 2 days ago

I see. Can you post the full example (e.g. the definition of S)? We can check what MIRI says.

artemagvanian commented 2 days ago

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

zhassan-aws commented 2 days ago

Got it. Thanks for the clarification.

model-checking / kani