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.

Sign up for GitHub

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

Jump to bottom

Missing check for object correctness invariants #301

Closed
danielsn opened this issue Jul 6, 2021 · 1 comment · Fixed by #3085
Closed

Missing check for object correctness invariants #301

danielsn opened this issue Jul 6, 2021 · 1 comment · Fixed by #3085
Labels
[E] Unsupported UB Undefined behavior that Kani does not detect
Milestone
Soundness

Comments

@danielsn
Copy link
Contributor

danielsn commented Jul 6, 2021 •
edited by celinval
Loading

Rust requires that all values have to be valid when assigned to or read from a place, passed to a function/primitive operation or returned from a function/primitive operation. It is UB to produce an invalid bit-pattern of a given type. We do not currently have any checks for this in Kani.

Likelihood:

If code contains this bug, Kani will not detect it. We do not have any data as to how often this occurs in practice.

Mitigation:

Warn users that this class of UB is outside the current scope of Kani.

Path to soundness:

Add a check for this.

Documentation:
@danielsn danielsn added this to the Soundness milestone Jul 8, 2021
@zhassan-aws zhassan-aws changed the title Soundness: Missing check for object correctness invariants Missing check for object correctness invariants Apr 19, 2022
@tedinski tedinski added the [E] Unsupported UB Undefined behavior that Kani does not detect label Nov 14, 2022
@celinval celinval mentioned this issue Mar 19, 2024
Merged
@celinval
Copy link
Contributor

I believe this is addressed by #3085 where we either add validity checks or we ICE. This feature is still unstable and its stabilization will be tracked in #2998

celinval added a commit that referenced this issue Mar 25, 2024
@celinval @zhassan-aws
Implement validity checks (#3085)
e4a90e9 
This is still incomplete, but hopefully it can be merged as an unstable
feature. I'll publish an RFC shortly.

This instruments the function body with assertion checks to see if users
are generating invalid values. This covers:
  - Union access
  - Raw pointer dereference
  - Transmute value
  - Field assignment of struct with invalid values
  - Aggregate assignment

Things not covered today should trigger ICE or a delayed verification
failure due to unsupported feature.

## Design

This change has two main design changes which are inside the new
`kani_compiler::kani_middle::transform` module:
1- Instance body should now be retrieved from the `BodyTransformation`
structure. This structure will run transformation passes on instance
bodies (i.e.: monomorphic instances) and cache the result.
2- Create a new transformation pass that instruments the body of a
function for every potential invalid value generation.
3- Create a body builder which contains all elements of a function body
and mutable functions to modify them accordingly.


Related to #2998
Fixes #301 

---------

Co-authored-by: Zyad Hassan <88045115+zhassan-aws@users.noreply.github.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
[E] Unsupported UB Undefined behavior that Kani does not detect
Projects
None yet
Milestone
Soundness
Development

Successfully merging a pull request may close this issue.

Implement validity checks celinval/kani-dev
4 participants
@tedinski @danielsn @celinval @zhassan-aws