Semantics of ZST dangling pointers: Kani differs from Miri

[fzaiser]

Dangling pointers in Rust are considered valid by Miri as long as they are not null, aligned, not deallocated, not out of bounds (if they have the provenance of some allocation) and we don't read or write more than zero bytes from/to the memory location they point to. By contrast, CBMC considers reading and writing from/to such dangling pointers to be UB, for example in memcmp(..., ..., 0).

This was originally discovered in #1489 but the same problem could occur with other functions than memcmp, so we should probably figure out a better way to deal with it. Previous discussion:

• discovery and some discussion: #1489
• mitigation for memcmp: #1526
• two examples that we should reject, but now accept due to shortcomings of the mitigation PR: https://github.com/model-checking/kani/issues/1489#issuecomment-1212553924, https://github.com/model-checking/kani/pull/1526#issuecomment-1221465620
• CBMC issue discussing pointer semantics: https://github.com/diffblue/cbmc/issues/7064.
• In particular, Daniel Kröning says: "Note that memcpy doesn't accept invalid pointers even when the size is zero." (https://github.com/diffblue/cbmc/issues/7064#issuecomment-1218275321). So the interpretation of the C standard seems to differ here.
• Documentation of pointers in CBMC: http://cprover.diffblue.com/memory-primitives.html

[RalfJung]

as long as they are not null, aligned, not deallocated and we don't read or write more than zero bytes from/to the memory location they point to

They must also not be OOB, if they do have the provenance of some allocation.

I wonder, how do you model Rust's wrapping_offset in CBMC? That also requires keep track of provenance for invalid pointers.

[RalfJung]

However, I should also note that these are just the current rules in Miri, not some final decision about Rust semantics. There are several threads in the UCG related to this question, e.g. https://github.com/rust-lang/unsafe-code-guidelines/issues/93.

[fzaiser]

They must also not be OOB, if they do have the provenance of some allocation.

@RalfJung Thanks, added

I don't know about wrapping_offset. Maybe @danielsn knows more?

[zhassan-aws]

Our modeling of the arith_offset intrinsic (which is called by wrapping_offset) is here: https://github.com/model-checking/kani/blob/cae7acaa08598d4f48ef6dd77e9b5b789230a90b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs#L1040

As the doc comment says, we currently don't check that the resulting pointer stays within bounds of the object.

[RalfJung]

Right, indeed it is okay for it to leave the bounds of the object.

But when the pointer is actually used, then it must be in-bounds of the offset it started out from. So this is an interesting test for provenance.

[zhassan-aws]

Kani supposedly handles the out-of-bounds pointer dereference correctly, e.g.:

#[cfg_attr(kani, kani::proof)]
fn main() {
    let arr = [1u8, 2, 3, 4, 5];
    let ptr1: *const u8 = arr.as_ptr();
    let ptr2 = ptr1.wrapping_offset(5);
    //let _v = unsafe { *ptr2 };
}

$ kani wrap.rs
<snip>
SUMMARY:
 ** 0 of 2 failed

VERIFICATION:- SUCCESSFUL

And uncommenting the let _v line results in:

SUMMARY:
 ** 1 of 8 failed
Failed Checks: dereference failure: pointer outside object bounds
 File: "/home/ubuntu/examples/wrap.rs", line 6, in main

VERIFICATION:- FAILED

[giltho]

Yes Kani handles wrapping offset very well, but it fails at detecting overflow for non-wrapping offset operators. Kani doesn't have checks for out-of-bound pointer before dereferencing them. I'd be curious about the peformance impact of adding those, but probably quite expensive :/

#[kani::proof]
fn main() {
    let x: [u32; 4] = [0, 1, 2, 3];
    let p = &x as *const [u32; 4] as *const u32;
    let _pp = unsafe { p.offset(1000) };
}

[giltho]

Actually, it's maybe not that expensive, Kanillian supports it and will correctly fail on that example

[celinval]

For CBMC to detect that case, we probably just need to explicitly add the boundary check after the offset call.

[celinval]

I believe this issue is related to https://github.com/model-checking/kani/issues/763. We used to enable CBMC's offset checks, but we decided to disable them.

[zhassan-aws]

Correct: running @giltho's example with:

kani offset.rs --enable-unstable --extra-pointer-checks

correctly reports the issue:

<snip>
Check 8: pointer_arithmetic.5
         - Status: FAILURE
         - Description: "pointer arithmetic: pointer outside object bounds"

[giltho]

Interesting, but then you indeed end up doing oob checks on dangling pointers which causes spurious errors.

In Kanillian, I model ZST pointers as "any non-0 usize with the right alignment". In the case of a ZST pointer, it means that the pointer could in theory have value (usize::MAX), and therefore offsetting it with any other value than 0 creates an out of bound pointer that is caught I don't think that model is perfect, but it does capture oob arithmetics for ZSTs and non-zst pointers without false-negative.

However, that means I'm not tracking pointer provenance, which is unsound

[RalfJung]

FWIW there are some arguments that might make us change MiniRust to allow UAF and OOB pointers for zero-sized accesses.

[giltho]

Reading threads and issues about ZST pointer arithmetics is such a rabbit hole, I've been reading these for the last 2 hours hahahaha It does feel a bit like a "unfortunately, we're based on LLVM" case

[RalfJung]

It does feel a bit like a "unfortunately, we're based on LLVM" case

Only in the sense that if we weren't based on LLVM I would advocate even more strongly in favor of making offset(0) just always allowed, and ZST derefs always allowed for aligned non-null pointers.

Also see this discussion.