diff --git a/zerocopy/src/macros.rs b/zerocopy/src/macros.rs index 717570ae6e..22d3c999d6 100644 --- a/zerocopy/src/macros.rs +++ b/zerocopy/src/macros.rs @@ -1253,6 +1253,344 @@ macro_rules! cryptocorrosion_derive_traits { }; } +#[cfg(kani)] +mod proofs { + use crate::{ + proof_support::{ + all_zero_byte_policy_oracle, assert_same_u8_elements, assert_same_usize, + bool_from_byte, copy_snapshot, + }, + TryFromBytes, ValidityError, + }; + + #[derive(TryFromBytes)] + #[repr(C, align(16))] + struct PaddedPointer { + pointer: *const u8, + } + + fn checked_bool_oracle(src: u8) -> Option { + bool_from_byte(src) + } + + fn cover_bool_oracle(expected: Option) { + kani::cover!(expected == Some(false)); + kani::cover!(expected == Some(true)); + kani::cover!(expected.is_none()); + } + + // Configuration: Uses the common Kani CI configuration documented in + // `agent_docs/validation.md`: the CI-pinned Kani release and its bundled + // x86_64-unknown-linux-gnu compiler, the stable-compatible feature bundle, + // `-Zfunction-contracts`, and one layout selected by `--randomize-layout` + // per invocation. + // + // Bool domain and oracle: `checked_bool_oracle` delegates only to the + // shared safe-Rust `bool_from_byte`, whose `u8::from(bool)` construction + // [1] and exhaustive language representation [2] are documented next to + // that helper. It neither invokes zerocopy nor consults the result under + // proof. Kani explores all 256 `u8` values, with covers for false, true, + // and invalid inputs. The value and reference macros are invoked only for + // the two independently valid representations; they check the decoded + // value, the explicit zerocopy same-address policy, and mutation + // propagation. `addr_of!` / `addr_of_mut!` obtain a raw pointer to the + // source place without creating an intermediate reference [5]. Rust's + // reference-to-raw coercions, sized pointer casts, and raw-pointer equality + // independently specify how both modeled addresses are observed [6][7]. + // Requiring them to match is a zerocopy policy oracle, not a Rust-language + // requirement, and establishes no provenance property. + // + // Owned-value pointer policy: Two independent harnesses exercise the + // owned-value macro. The first covers every `usize` as a direct + // `*const u8` candidate. Safe `usize::to_ne_bytes` obtains its exact memory + // representation [8], and the shared `all_zero_byte_policy_oracle` + // classifies the complete eight-byte array through a Rust repeat array, + // safe iteration, and primitive equality. The helper's adjacent docs give + // those exact Rust 1.93 contracts; it never reconstructs an integer or + // calls zerocopy. This family separately adopts all-zero acceptance as the + // explicit conservative zerocopy pointer policy under test. + // + // The second harness covers every `[u8; 16]` source and transmutes to + // `PaddedPointer`. Pinned compiler observations require an eight-byte thin + // pointer at offset zero in a 16-byte, 16-aligned `repr(C)` destination; + // the remaining eight bytes are therefore genuine destination tail + // padding [10][11]. Safe `slice::first_chunk` obtains exactly the first + // eight source bytes, with `Option::expect` making a missing chunk fail + // closed [9]. The same shared all-zero classifier supplies the pointer-field + // policy while deliberately ignoring the padding bytes. The derived + // `TryFromBytes` validator is part of the target path, not an oracle. The + // end-to-end harness proves, rather than assumes, that macro acceptance + // matches that field policy and is independent of the padding. Covers + // witness acceptance and rejection with nonzero padding but do not + // constrain the universal input domain. On every rejection, the shared + // ordered-byte observer compares all 16 returned source bytes with a safe + // pre-call snapshot. It projects the crate-visible error field rather than + // calling `ValidityError::into_src`, preventing accessor and macro defects + // from compensating. + // + // Mutable-bool write-back: The replacement `!expected` is computed from + // the independent checked-bool oracle before the target is invoked. For a + // `bool`, logical negation exchanges `true` and `false` [14]. Built-in + // dereference of `&mut bool` denotes the pointed-to assignable place, and + // assignment copies the independently computed right-hand value into that + // place [14]. After the target reference's last use, safe `u8::from` + // supplies the expected source representation [1], and primitive `u8` + // equality supplies the final observation [15]. None of those operations + // consults zerocopy to construct the expected mutation or result. + // + // Destination validity and accepted value: Rust guarantees that every + // integer representation can validly produce a thin raw pointer [3]; + // [10][11] establish that bytes 8 through 15 are destination tail padding, + // and Rust expressly permits uninitialized memory in padding [12]. We use + // that language rule as the TCB premise that those padding bytes impose no + // additional value-validity constraint; Kani does not prove that premise. + // Thus an erroneous acceptance in either pointer harness still cannot + // materialize an invalid destination. On the accepted all-zero field, safe + // `core::ptr::null()` independently supplies the expected pointer by its + // standard-library contract [4]. Neither harness dereferences the result. + // + // Storage and bounds: Each bool harness uses one stack `u8`; the direct + // pointer harness uses one `usize` and its eight-byte representation. The + // padded harness uses one 16-byte source plus its safe snapshot; all other + // values are fixed-size compiler temporaries. No harness allocates, + // contains an explicit source loop, or uses `kani::assume`; every symbolic + // input is unconstrained. Bool harnesses use unwind one. The direct pointer + // harness uses unwind nine for an eight-byte target/helper scan plus + // termination. The padded harness uses unwind 17 for its 16-byte recovery + // comparison plus termination. Kani's unwinding checks enforce each bound. + // + // Scope and TOOL/TCB boundary: These are end-to-end proofs only for the + // listed `u8`-to-`bool`, `usize`-to-`*const u8`, and + // `[u8; 16]`-to-`PaddedPointer` instantiations on the pinned target. They do + // not prove other types, padding shapes, sizes, alignments, macro arms, or + // toolchains. Invalid-bool public paths remain uninvoked because Kani does + // not completely check invalid-value production. Reading and writing the + // reference-macro results presupposes live, dereferenceable references with + // valid lifetime, aliasing, and provenance; Kani does not completely check + // those obligations, so they remain TOOL/TCB premises rather than proof + // conclusions. Its uninitialized-memory/padding model is likewise a + // premise for the padded recovery result. In particular, this harness also + // verifies when the target body is locally replaced with the typed + // `MaybeUninit>` implementation immediately before + // 94f0da71; Kani does not expose that implementation's compiler-permitted + // destination-padding loss. The theorem therefore observes every + // initialized source byte on `Err` in Kani's selected execution model, but + // is not regression evidence for #3632/#3634 or a proof over every + // compiler-permitted padding behavior. It does not observe destination + // padding after `Ok`. Reference-arm error recovery is not exercised. + // + // [1] Per https://doc.rust-lang.org/1.93.0/std/primitive.u8.html#impl-From%3Cbool%3E-for-u8: + // + // Converts from `bool` to `u8`, by turning `false` into `0` and `true` + // into `1`. + // + // [2] Per https://doc.rust-lang.org/1.93.0/reference/types/boolean.html#representation: + // + // The value false has the bit pattern `0x00` and the value true has the + // bit pattern `0x01`. It is undefined behavior for an object with the + // boolean type to have any other bit pattern. + // + // [3] Per https://doc.rust-lang.org/1.93.0/reference/types/pointer.html#bit-validity: + // + // For thin raw pointers (i.e., for `P = *const T` or `P = *mut T` for + // `T: Sized`), the inverse direction (transmuting from an integer or + // array of integers to `P`) is always valid. However, the pointer + // produced via such a transmutation may not be dereferenced (not even + // if `T` has size zero). + // + // [4] Per https://doc.rust-lang.org/1.93.0/std/ptr/fn.null.html: + // + // Creates a null raw pointer. + // + // This function is equivalent to zero-initializing the pointer: + // `MaybeUninit::<*const T>::zeroed().assume_init()`. The resulting + // pointer has the address 0. + // + // [5] Per https://doc.rust-lang.org/1.93.0/std/ptr/macro.addr_of.html and + // https://doc.rust-lang.org/1.93.0/std/ptr/macro.addr_of_mut.html: + // + // Creates a `const` raw pointer to a place, without creating an + // intermediate reference. + // + // Creates a `mut` raw pointer to a place, without creating an + // intermediate reference. + // + // [6] Rust 1.93 lists the coercions “`&T` to `*const T`” and “`&mut T` to + // `*mut T`”: + // https://doc.rust-lang.org/1.93.0/reference/type-coercions.html#coercion-types + // + // [7] For sized pointer-to-pointer casts, Rust 1.93 says “the pointer is + // returned unchanged”; raw-pointer `PartialEq` says “Pointer equality is + // by address”: + // https://doc.rust-lang.org/1.93.0/reference/expressions/operator-expr.html#pointer-to-pointer-cast + // https://doc.rust-lang.org/1.93.0/std/primitive.pointer.html#impl-PartialEq-for-*const+T + // https://doc.rust-lang.org/1.93.0/std/primitive.pointer.html#impl-PartialEq-for-*mut+T + // + // [8] Per https://doc.rust-lang.org/1.93.0/std/primitive.usize.html#method.to_ne_bytes: + // + // Returns the memory representation of this integer as a byte array in + // native byte order. + // + // [9] Rust 1.93 specifies that `first_chunk` returns a reference to the + // first `N` items, or `None` when the slice is shorter; `Option::expect` + // returns `Some` and panics for `None`: + // https://doc.rust-lang.org/1.93.0/std/primitive.slice.html#method.first_chunk + // https://doc.rust-lang.org/1.93.0/std/option/enum.Option.html#method.expect + // + // [10] Rust 1.93 specifies the `repr(C)` struct layout algorithm and that + // `align(N)` raises a type's alignment to at least `N`: + // https://doc.rust-lang.org/1.93.0/reference/type-layout.html#reprc-structs + // https://doc.rust-lang.org/1.93.0/reference/type-layout.html#the-alignment-modifiers + // + // [11] Rust 1.93 specifies the compiler layout observations used by the + // fail-closed pinned-target assertions: + // https://doc.rust-lang.org/1.93.0/core/mem/fn.size_of.html + // https://doc.rust-lang.org/1.93.0/core/mem/fn.align_of.html + // https://doc.rust-lang.org/1.93.0/core/mem/macro.offset_of.html + // + // [12] https://doc.rust-lang.org/1.93.0/reference/behavior-considered-undefined.html#invalid-values + // [13] https://doc.rust-lang.org/1.93.0/reference/expressions.html#moved-and-copied-types + // https://doc.rust-lang.org/1.93.0/std/primitive.usize.html#impl-Copy-for-usize + // [14] https://doc.rust-lang.org/1.93.0/reference/types/boolean.html#logical-not + // https://doc.rust-lang.org/1.93.0/reference/expressions/operator-expr.html#the-dereference-operator + // https://doc.rust-lang.org/1.93.0/reference/expressions/assignment-expr.html + // [15] https://doc.rust-lang.org/1.93.0/std/macro.assert_eq.html + // https://doc.rust-lang.org/1.93.0/std/primitive.u8.html#impl-PartialEq-for-u8 + + #[kani::proof] + #[kani::unwind(1)] + fn prove_try_transmute_u8_to_bool() { + let src: u8 = kani::any(); + let expected = checked_bool_oracle(src); + cover_bool_oracle(expected); + if let Some(expected) = expected { + let result: Result> = crate::try_transmute!(src); + match result { + Ok(dst) => assert_eq!(dst, expected), + Err(_) => panic!("transmute rejected an independently valid bool"), + } + } + } + + #[kani::proof] + #[kani::unwind(1)] + fn prove_try_transmute_ref_u8_to_bool() { + let src: u8 = kani::any(); + let src_ptr = core::ptr::addr_of!(src); + let expected = checked_bool_oracle(src); + cover_bool_oracle(expected); + if let Some(expected) = expected { + let result: Result<&bool, ValidityError<&u8, bool>> = crate::try_transmute_ref!(&src); + match result { + Ok(dst) => { + assert_eq!((dst as *const bool).cast::(), src_ptr); + assert_eq!(*dst, expected); + } + Err(_) => panic!("reference transmute rejected an independently valid bool"), + } + } + } + + #[kani::proof] + #[kani::unwind(1)] + fn prove_try_transmute_mut_u8_to_bool() { + let mut src: u8 = kani::any(); + let src_ptr = core::ptr::addr_of_mut!(src); + let expected = checked_bool_oracle(src); + cover_bool_oracle(expected); + if let Some(expected) = expected { + let expected_after_mutation = !expected; + let result: Result<&mut bool, ValidityError<&mut u8, bool>> = + crate::try_transmute_mut!(&mut src); + match result { + Ok(dst) => { + assert_eq!((dst as *mut bool).cast::(), src_ptr); + assert_eq!(*dst, expected); + *dst = expected_after_mutation; + } + Err(_) => panic!("mutable transmute rejected an independently valid bool"), + } + assert_eq!(src, u8::from(expected_after_mutation)); + } + } + + #[kani::proof] + #[kani::unwind(9)] + // This transmutation is the operation under proof. The resulting pointer + // is valid to produce by [3] and is never dereferenced. Safe + // `usize::to_ne_bytes` [8] plus the shared complete-array classifier supply + // the independently observed bytes to which this family applies its + // explicit zero-only pointer policy. Safe `core::ptr::null()` is the + // expected result on that branch by [4]. Before the target consumes its + // `usize` source, the shared `copy_snapshot` takes an independent safe-Rust + // pre-call value snapshot. Its documented dereference/value-expression + // kernel copies the value because `usize: Copy` [13]. On rejection, direct + // projection of the crate-visible error field avoids + // `ValidityError::into_src`, and the shared `assert_same_usize` supplies + // primitive `usize` equality independently of the target. Accessor and + // macro defects therefore cannot compensate. + // `#[allow(unknown_lints)]` is for `integer_to_ptr_transmutes` on the MSRV. + #[allow(unknown_lints)] + #[allow(integer_to_ptr_transmutes)] + fn prove_try_transmute_usize_to_pointer_policy_and_recovery() { + let src: usize = kani::any(); + let expected_src = copy_snapshot(&src); + let src_bytes = expected_src.to_ne_bytes(); + let expected_valid = all_zero_byte_policy_oracle(&src_bytes); + let result: Result<*const u8, ValidityError> = crate::try_transmute!(src); + + kani::cover!(expected_valid); + kani::cover!(!expected_valid); + match result { + Ok(pointer) => { + assert!(expected_valid); + assert_eq!(pointer, core::ptr::null()); + } + Err(error) => { + assert!(!expected_valid); + assert_same_usize(error.src, expected_src); + } + } + } + + #[kani::proof] + #[kani::unwind(17)] + fn prove_try_transmute_padded_pointer_policy_and_recovery() { + const POINTER_BYTES: usize = 8; + const OBJECT_BYTES: usize = 16; + + assert_same_usize(core::mem::size_of::<*const u8>(), POINTER_BYTES); + assert_same_usize(core::mem::align_of::(), OBJECT_BYTES); + assert_same_usize(core::mem::size_of::(), OBJECT_BYTES); + assert_same_usize(core::mem::offset_of!(PaddedPointer, pointer), 0); + assert!(core::mem::size_of::() > core::mem::size_of::<*const u8>()); + + let src: [u8; OBJECT_BYTES] = kani::any(); + let snapshot = copy_snapshot(&src); + let pointer_bytes = snapshot + .first_chunk::() + .expect("a 16-byte source must contain its eight-byte pointer field"); + let expected_valid = all_zero_byte_policy_oracle(pointer_bytes); + let result: Result> = + crate::try_transmute!(src); + + kani::cover!(expected_valid); + kani::cover!(!expected_valid); + kani::cover!(expected_valid && snapshot[POINTER_BYTES] != 0); + kani::cover!(!expected_valid && snapshot[POINTER_BYTES] != 0); + match result { + Ok(dst) => { + assert!(expected_valid); + assert_eq!(dst.pointer, core::ptr::null()); + } + Err(error) => { + assert!(!expected_valid); + assert_same_u8_elements(&error.src, &snapshot); + } + } + } +} + #[cfg(test)] mod tests { use crate::{