Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Uninitialized memory detection mitigates delayed UB, but does not support it fully #3324

Closed
celinval opened this issue Jul 4, 2024 · 1 comment · Fixed by #3332 or #3374
Closed
Assignees
Labels
[E] Unsupported UB Undefined behavior that Kani does not detect Z-UnstableFeature Issues that only occur if a unstable feature is enabled

Comments

@celinval
Copy link
Contributor

celinval commented Jul 4, 2024

I tried this code:

#[kani::proof]
fn invalid_value() {
    unsafe {
        let mut value: u128 = 0;
        let ptr = &mut value as *mut _ as *mut (u8, u32, u64);
        *ptr = (4, 4, 4);   // This assignment itself does not cause UB...
        assert!(value > 0); // ...but this reads a padding value! ⚠️
    }
}

using the following command line invocation:

kani -Z ghost-state -Z uninit-checks delayed-ub.rs

with Kani version: 0.53

I expected to see this happen: Verification should fail since we are reading padding values.

Instead, this happened: Verification succeed

@celinval celinval added [C] Bug This is a bug. Something isn't working. [F] Soundness Kani failed to detect an issue labels Jul 4, 2024
@celinval celinval added the Z-UnstableFeature Issues that only occur if a unstable feature is enabled label Jul 4, 2024
@artemagvanian artemagvanian reopened this Jul 12, 2024
@artemagvanian artemagvanian changed the title Uninitialized memory detection misses delayed UB Uninitialized memory detection mitigates delayed UB, but does not support it fully Jul 12, 2024
@artemagvanian
Copy link
Contributor

#3332 mitigated the issue: now all mutable pointer casts of unsupported padding are rejected

@artemagvanian artemagvanian added [E] Unsupported UB Undefined behavior that Kani does not detect and removed [C] Bug This is a bug. Something isn't working. [F] Soundness Kani failed to detect an issue labels Jul 12, 2024
artemagvanian added a commit that referenced this issue Jul 16, 2024
This PR addresses another aspect of #3324, where delayed UB could be
caused by transmuting a mutable pointer into the one of incompatible
padding. It also adds a check to error whenever transmuting between two
types of incompatible padding.

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.
artemagvanian added a commit that referenced this issue Jul 19, 2024
This PR adds basic support for global transformations, which will be
useful to implement full support of #3324

Changes:
- Add edge annotations to the call graph
- Implement global transformation pass infrastructure
- Implement `dump_mir` as a global transformation pass

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.

---------

Co-authored-by: Celina G. Val <celinval@amazon.com>
github-merge-queue bot pushed a commit that referenced this issue Aug 5, 2024
)

As #3324 mentioned, delayed UB triggered by accessing uninitialized
memory was previously mitigated by injecting `assert!(false)` for every
possible source of it; this PR adds all the necessary infrastructure and
minimal support for detecting it properly.

The process of detecting and instrumenting places is as follows:
- Find all sources of delayed uninitialized memory UB (mutable pointer
casts with different pointee padding and copy intrinsics);
- Compute conservative aliasing graph between all memory places
reachable from each harness;
- Instrument all places pointed to by each source we found in step 1.

Not all language constructs are currently supported -- see the tracking
issue (#3300) for the full list of limitations.

Resolves #3324

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.

---------

Co-authored-by: Celina G. Val <celinval@amazon.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
[E] Unsupported UB Undefined behavior that Kani does not detect Z-UnstableFeature Issues that only occur if a unstable feature is enabled
Projects
None yet
2 participants