Fix OffsetModel missing UB for offsets wrapping CBMC's pointer encoding#4671
Open
tautschnig wants to merge 1 commit into
Open
Fix OffsetModel missing UB for offsets wrapping CBMC's pointer encoding#4671tautschnig wants to merge 1 commit into
tautschnig wants to merge 1 commit into
Conversation
CBMC encodes pointers as an (object, offset) pair where the offset field has pointer_width - object_bits bits. Pointer arithmetic therefore wraps offsets at 2^(64 - object_bits) rather than 2^64 (model-checking#1150). For the OffsetModel this meant that a symbolic byte offset that is a non-zero multiple of 2^(64 - object_bits) (2^48 with Kani's default of 16 object bits) made `wrapping_byte_offset` alias the original pointer, so the subsequent same-allocation safety check passed spuriously and genuine out-of-bounds `offset` calls verified successfully - including "proving" the false fact that the result equals the base pointer. Detect the wrap by additionally requiring that the address of the result is consistent with full-width integer arithmetic on the address of the original pointer; any truncation in the pointer addition falsifies this equation. Two alternative formulations do not work: * Computing the new pointer via integer arithmetic (addr().wrapping_add_signed(off) followed by a cast back, as previously suggested in a FIXME here) is sound, but makes the solver case-split the integer address over every object; harnesses using e.g. `sort()` then run out of memory. These are the "unexpected failures" mentioned in the removed comment (reproduced on: expected/cover/cover-pass, expected/string-repeat, expected/loop-backedge, expected/shadow/unsupported_num_objects). * Comparing POINTER_OFFSET(new) against full-width POINTER_OFFSET(orig) + offset is defeated by CBMC's simplifier, which rewrites POINTER_OFFSET(p + k) to POINTER_OFFSET(p) + k in full-width arithmetic, making the equation trivially true. The `addr()` transmute is opaque to that simplification, keeps all operations in the pointer domain, and adds negligible solver cost: the full expected (459) and kani (593) suites pass unchanged. The underlying encoding wrap is fixed on the CBMC side in diffblue/cbmc#9134 (out-of-range results are directed to the invalid object). The equation here also states Rust's address-arithmetic contract for `offset` and produces the same verdicts with and without that CBMC fix, so it is kept as a semantic guard rather than a version-specific workaround. Partially addresses model-checking#1150: this fixes the missed-UB soundness hole in the checked `offset`/`arith_offset` intrinsic model. Not addressed is the `wrapping_offset` family, which Kani codegens to plain CBMC pointer addition: under CBMC versions without the encoding fix its result aliases the base pointer for wrap-multiple offsets (tests/kani/PointerOffset/fixme_wrap_nonzero_offset.rs), and even with the CBMC fix the result address is indeterminate rather than the exactly-wrapped address that Rust defines. Exact modeling would require integer arithmetic plus an integer-to-pointer cast, which makes the solver case-split over all objects (see above). Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
github-actions
Bot
added
Z-EndToEndBenchCI
Contributor
There was a problem hiding this comment.
Pull request overview
This pull request strengthens Kani’s OffsetModel safety checking to detect and reject undefined behavior that was previously missed due to CBMC’s pointer encoding truncating/wrapping the offset field (issue #1150), and adds a regression test to ensure the soundness hole stays closed across CBMC versions.
Changes:
- Add an address-consistency guard (
addr()-based) to detect offset truncation/wrap in CBMC’s pointer encoding before relying on same-allocation checks. - Add a new expected-suite regression test covering symbolic high-offset wrap cases (positive, negative, and
isize::MIN), plus an in-bounds control harness. - Add corresponding
.expectedoutput asserting the new failures are reported.
Reviewed changes
Copilot reviewed 3 out of 3 changed files in this pull request and generated 2 comments.
| File | Description |
|---|---|
| tests/expected/offset-bounds-check/offset_wrap_sym.rs | New regression harnesses exercising the high-offset wrap soundness hole and a valid in-bounds negative-offset case. |
| tests/expected/offset-bounds-check/offset_wrap_sym.expected | Expected output for the new regression tests (3 failures, 1 success). |
| library/kani_core/src/models.rs | Tightens OffsetModel UB detection by adding an address-arithmetic consistency check alongside same-allocation checking. |
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
| // address over every object and blow up, e.g., on harnesses using | ||
| // `sort()`). | ||
| let new_ptr = orig_ptr.wrapping_byte_offset(byte_offset); | ||
| let no_wrap = new_ptr.addr() == orig_ptr.addr().wrapping_add(byte_offset as usize); |
Comment on lines
158
to
161
| kani::safety_check( | ||
| kani::mem::same_allocation_internal(orig_ptr, new_ptr), | ||
| no_wrap && kani::mem::same_allocation_internal(orig_ptr, new_ptr), | ||
| "Offset result and original pointer must point to the same allocation", | ||
| ); |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
CBMC encodes pointers as an (object, offset) pair where the offset field has pointer_width - object_bits bits. Pointer arithmetic therefore wraps offsets at 2^(64 - object_bits) rather than 2^64 (#1150). For the OffsetModel this meant that a symbolic byte offset that is a non-zero multiple of 2^(64 - object_bits) (2^48 with Kani's default of 16 object bits) made
wrapping_byte_offsetalias the original pointer, so the subsequent same-allocation safety check passed spuriously and genuine out-of-boundsoffsetcalls verified successfully - including "proving" the false fact that the result equals the base pointer.Detect the wrap by additionally requiring that the address of the result is consistent with full-width integer arithmetic on the address of the original pointer; any truncation in the pointer addition falsifies this equation. Two alternative formulations do not work:
Computing the new pointer via integer arithmetic (addr().wrapping_add_signed(off) followed by a cast back, as previously suggested in a FIXME here) is sound, but makes the solver case-split the integer address over every object; harnesses using e.g.
sort()then run out of memory. These are the "unexpected failures" mentioned in the removed comment (reproduced on: expected/cover/cover-pass, expected/string-repeat, expected/loop-backedge, expected/shadow/unsupported_num_objects).Comparing POINTER_OFFSET(new) against full-width POINTER_OFFSET(orig) + offset is defeated by CBMC's simplifier, which rewrites POINTER_OFFSET(p + k) to POINTER_OFFSET(p) + k in full-width arithmetic, making the equation trivially true.
The
addr()transmute is opaque to that simplification, keeps all operations in the pointer domain, and adds negligible solver cost: the full expected (459) and kani (593) suites pass unchanged.The underlying encoding wrap is fixed on the CBMC side in diffblue/cbmc#9134 (out-of-range results are directed to the invalid object). The equation here also states Rust's address-arithmetic contract for
offsetand produces the same verdicts with and without that CBMC fix, so it is kept as a semantic guard rather than a version-specific workaround.Partially addresses #1150: this fixes the missed-UB soundness hole in the checked
offset/arith_offsetintrinsic model. Not addressed is thewrapping_offsetfamily, which Kani codegens to plain CBMC pointer addition: under CBMC versions without the encoding fix its result aliases the base pointer for wrap-multiple offsets (tests/kani/PointerOffset/fixme_wrap_nonzero_offset.rs), and even with the CBMC fix the result address is indeterminate rather than the exactly-wrapped address that Rust defines. Exact modeling would require integer arithmetic plus an integer-to-pointer cast, which makes the solver case-split over all objects (see above).By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.