Tracking Issue: Automatically Verify Memory Initialization

[artemagvanian]

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 (Towards Proving Memory Initialization #3264)
• Make sure layout representation does not negatively affect performance (Improve performance and language support of memory initialization checks #3313)
• Fix behavior of copy and copy_nonoverlapping (Checking memory initialization in presence of copy and copy_nonoverlapping produces false positives #3347, Implement memory initialization state copy functionality  #3350)
• Add support for delayed UB via static analysis (Uninitialized memory detection mitigates delayed UB, but does not support it fully #3324, Instrumentation for delayed UB stemming from uninitialized memory #3374)
  • Handle intrinsics systematically (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 (Add better support for MaybeUninit #896)
  • Unions can be created, assigned to, read from (Basic support for memory initialization checks for unions #3444)
  • Unions can be passed as arguments to other functions (Cross-function union instrumentation #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

[zhassan-aws]

// ~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]

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

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

[artemagvanian]

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]

Got it. Thanks for the clarification.