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