diff --git a/rfc/src/SUMMARY.md b/rfc/src/SUMMARY.md index 2fb7d0b133cd..dc6bcf1aefbf 100644 --- a/rfc/src/SUMMARY.md +++ b/rfc/src/SUMMARY.md @@ -19,3 +19,4 @@ - [0011-source-coverage](rfcs/0011-source-coverage.md) - [0012-loop-contracts](rfcs/0012-loop-contracts.md) - [0013-list](rfcs/0013-list.md) +- [0014-rust-ub-checks](rfcs/0014-rust-ub-checks.md) diff --git a/rfc/src/rfcs/0014-rust-ub-checks.md b/rfc/src/rfcs/0014-rust-ub-checks.md new file mode 100644 index 000000000000..b2fbc3089dd9 --- /dev/null +++ b/rfc/src/rfcs/0014-rust-ub-checks.md @@ -0,0 +1,187 @@ +- **Feature Name:** Rust UB Checks (`rust-ub-checks`) +- **Feature Request Issue:** [#3089](https://github.com/model-checking/kani/issues/3089) +- **RFC PR:** [#3091](https://github.com/model-checking/kani/pull/3091) +- **Status:** Unstable +- **Version:** 0 +- **Proof-of-concept:** + +------------------- + +## Summary + +Specify a consistent framework for Undefined Behavior (UB) checks in Kani. + +## User Impact + +Provide a consistent user experience for all UB checks in Kani, while establishing the best mechanisms for +further instrumentation of undefined behavior in Kani. + +## User Experience + +A UB check should behave consistently independent on how and where it is implemented. +The detection of an undefined behavior should impact the status of any assertion that may be reachable from the +detected undefined behavior. + +For simplicity, we propose that all undefined behavior checks are modelled as assert-assume pairs. +We propose that the status of all passing assertions that may be affected by this check to be displayed as +`UNDETERMINED` if one or more UB checks fail. +For simplicity, Kani currently over-approximate this set by marking all passing assertions as `UNDETERMINED`. +Future pruning of this set can be done with further analysis, but it should not affect soundness. + +All failing assertions will have their status preserved. +This may create spurious counter examples for cases where the failing UB check is implemented using "demonic" +non-determinism.[^demonic] + +[^demonic]: Some UB checks implementation use one tracker with non-deterministic assignment to track the +status of different objects. +This implementation relies on the fact that an assertion will fail if there is at least one possible +assignment to its tracker that violates the assertion. +Picking an assignment that fails can be seen as choosing the worst possible action, known as demonic nondeterminism. + +See [Open questions section](0010-rust-ub-checks.md#open-questions) for alternatives to be considered. + +### Concrete playback of UB checks + +A counter example that triggers UB may require extra tooling for debugging, e.g.: MIRI or valgrind. +We propose that tests added by concrete playback in those cases should include a comment stating such limitation. +Other possibilities are discussed in [0010-rust-ub-checks.md#open-questions]. + +### Delayed undefined behavior + +In some cases, undefined behavior may occur in safe code that interacts with unsafe code. + +For example, the code below shows how reading a boolean value in safe code may trigger UB due to an +invalid write: + +```rust +#[kani::proof] +fn buggy_code() { + let mut value: bool = false; + let ptr: *mut bool = &mut value as *mut _; + let mut_ref = &mut value; + unsafe { + *ptr = true; // This assignment is safe if `mut_ref` is never used! + } + assert!(!*mut_ref); // This triggers UB ⚠️! +} +``` + +It may not be scalable for Kani to verify that every value produced is valid. +In cases like that, we may opt for implementing one of the following UB checks: + +1. Perform static analysis to first identify which code may be affected by unsafe code, and only instrument those that + are reachable from the unsafe code. +2. Add eager UB detection in unsafe code that will fail verification if there are side effects that we may not be + able to detect efficiently. For example, we could fail if casting between types that have different value + requirements, i.e.: fail in the cast `*mut bool as *mut u8`. + +For option 2, Kani may fail verification even if the code does not have UB. +In those cases, Kani check must be explicit about this failure being an over-approximation. +For that, we propose that the check message is clear about this limitation, and potentially its status +(see [0010-rust-ub-checks.md#open-questions]). + +### Opt-out of a class of UB checks + +Undefined behavior checks that have been stabilized should be added by default by Kani. +However, Kani should provide a fine-grained control for users to choose which checks to disable. + +For every class of UB checks to be added, we shall add a command line argument to disable the check for all harnesses, +as well as an attribute that would allow users to opt-out a check for specific harnesses. + +Command line arguments should follow the existing name schema: +`--no-[CHECK-NAME]-checks` where the CHECK-NAME is kebab case. There is no need to add `--[CHECK-NAME]-checks` since +they are enabled by default. + +We propose to add the following attribute: + +```rust +#[kani::proof] +#[kani::ignore(CHECK_NAMES)] +fn harness() {} +``` + +Where `CHECK_NAMES` is a list of check category names in snake case, such as `memory_safety`, `valid_values`. + +For checks that are unstable, they should only be included if their respective unstable flag are passed, i.e., +`-Z [CHECK-NAME]`. + +## Software Design + +*To be filled in the next iteration* + +## Rationale and alternatives + +Kani already has undefined behavior checks, some are implemented on the CBMC side, such as access out bounds, and +arithmetic overflow. +While others are implemented on Kani's side, such as intrinsics validation checks, and some are a +result of instrumentation to the Rust standard library. + +The behavior of these checks varies according to how they are added. +The ones on CBMC side do not interrupt the analysis of a path, while the ones on Kani / Rust std side will. + +For example, memory bound checks are implemented in CBMC, and the following harness today will trigger 2 different +failures: + +```rust +#[kani::proof] +pub fn is_zero() { + let var = [0u32; 4]; + let ptr = &var as *const u32; + let idx: usize = 4; + assert_eq!(unsafe { ptr.add(idx).read() }, 0); +} +``` + +The failed checks are: + +```plaintext +Failed Checks: assertion failed: unsafe { ptr.add(idx).read() } == 0 +Failed Checks: dereference failure: pointer outside object bounds +``` + +While the following harness only fails the standard library check: + +```rust +#[kani::proof] +pub fn is_zero() { + let var = [0; 4]; + let idx: usize = 4; + assert_eq!(unsafe { *var.get_unchecked(idx) }, 0); +} +``` + +Failing due to an assumption check inside `get_unchecked` function. + +```plaintext +Failed Checks: assumption failed +``` + +We would like to keep taking advantage of existing instrumentation to maximize the UB check coverage. +The mechanism used to build the check, however, shouldn't influence in the user experience. + +### Opt-out vs opt-in + +The default behavior matches the one that we believe is the recommended for most users due to soundness. +In some cases, users may need to disable some checks for reasons such as spurious CEX or proof scalability. +Thus, we suggest that every category of checks should have an opt-out mechanism that can either be global or local; +i.e.: via command argument or harness attribute. + +The main disadvantage of this model is that stabilizing a new check category is a non-backward compatible change. +I.e.: It may impact the status of a previously passing harness if a new check fails. + +## Open questions + +- Should we add a new status for potentially spurious counter examples? Such as: + - Counter examples detected together with a non-deterministic UB check. + - Over-approximating UB checks. +- How should UB checks affect concrete playback? Is a comment enough? + - Another possibility would be to add a `unreachable!()` statement at the end of the test case with a message + explaining why the statement should be unreachable. +- Should we deprecate the `--no-default-checks` and all `--[CHECK-NAME]-checks` checks. +- Should we add an attribute that allows us to opt-out some UB checks for a function or some code block? + - I think we should at least consider adding that option for `kani` library code. + - We've been adding more logic that is used by UB checks, and we may want to skip some checks for them. + +## Out of scope / Future Improvements + +- **List enabled checks:** Kani could include a command that list all the categories of undefined behaviors supported.