search

model-checking / kani

Kani Rust Verifier
https://model-checking.github.io/kani
Apache License 2.0
2.17k stars 86 forks source link

Contract implementation is unsafe and may trigger UB #3293

Open celinval opened 3 months ago

celinval commented 3 months ago

Looking at the kani::internal::Pointer implementation for *mut T:

https://github.com/model-checking/kani/blob/1491dd6eaf453efc61e915e0a3d247c2ce03abaf/library/kani/src/internal.rs#L59-L63

This can trigger UB if the location pointed by *mut T does not contain a valid value of type T since it is converting it to a &T. Converting *const T into &mut T and *mut T to &mut T is also unsafe, and may break aliasing rules.

celinval commented 2 months ago

Note that https://github.com/model-checking/kani/pull/3363 removes the decouple_lifetime function, but untracked_deref function is still unsafe and my cause UB for arguments that are dropped inside the function.

I was wondering if we can use something similar to Prusti's snapshots: https://viperproject.github.io/prusti-dev/dev-guide/encoding/types-snap.html to replace untracked_deref.