|
| 1 | +# Soundness |
| 2 | + |
| 3 | +This page documents Kani's soundness guarantees and known limitations. |
| 4 | + |
| 5 | +## What Kani Checks |
| 6 | + |
| 7 | +Kani automatically checks for the following classes of issues: |
| 8 | + |
| 9 | +### Always enabled |
| 10 | +- **Arithmetic overflow**: Addition, subtraction, multiplication, division, |
| 11 | + remainder, shift, and negation on integer types. |
| 12 | +- **Division by zero**: Integer and floating-point division and remainder. |
| 13 | +- **Pointer dereference validity**: Null pointers, dangling pointers, pointers |
| 14 | + to deallocated or dead objects, out-of-bounds pointers, misaligned pointers. |
| 15 | +- **Array bounds**: Index out of bounds on arrays and slices. |
| 16 | +- **Panics**: `assert!`, `unwrap()`, `expect()`, `panic!()`, `unreachable!()`, |
| 17 | + and any other panic path in the code under verification. |
| 18 | +- **Shift distance**: Negative shift amounts and shifts exceeding the bit width. |
| 19 | +- **Float-to-integer conversion**: Non-finite float values (NaN, infinity) |
| 20 | + are rejected before conversion to integer types. |
| 21 | +- **Memory leaks**: Dynamically allocated memory that is never freed (within |
| 22 | + the verification scope). |
| 23 | + |
| 24 | +### Opt-in (unstable) |
| 25 | +- **Valid value invariants** (`-Z valid-value-checks`): Checks that values meet |
| 26 | + their type's validity requirements (e.g., `bool` is 0 or 1, `char` is a valid |
| 27 | + Unicode scalar value, enum discriminants are in range). This is an unstable |
| 28 | + feature that may change. |
| 29 | +- **Uninitialized memory** (`-Z uninit-checks`): Checks that memory is |
| 30 | + initialized before being read through pointers. This is an unstable feature |
| 31 | + that may change. |
| 32 | + |
| 33 | +## What Kani Does NOT Check |
| 34 | + |
| 35 | +The following classes of undefined behavior are **not detected** by Kani: |
| 36 | + |
| 37 | +- **Data races**: Kani verifies sequential code only. Concurrent programs are |
| 38 | + not supported. |
| 39 | +- **Pointer aliasing violations** (Stacked Borrows / Tree Borrows): Kani does |
| 40 | + not track reference lifetimes or enforce Rust's aliasing rules. If aliasing |
| 41 | + violations cause a memory safety or assertion failure, Kani will detect the |
| 42 | + symptom but not the root cause. |
| 43 | +- **Mutation of immutable data**: Same as aliasing — detected only if it causes |
| 44 | + an observable failure. |
| 45 | +- **Incorrect use of inline assembly**: Kani does not support inline assembly. |
| 46 | + Global assembly (`global_asm!`) is ignored with a warning. |
| 47 | +- **ABI violations**: Kani relies on `rustc` for ABI checking. |
| 48 | +- **Transmute to invalid values**: `kani::any()` always produces valid values, |
| 49 | + but `transmute` of invalid bit patterns is not detected unless the unstable |
| 50 | + `-Z valid-value-checks` flag is enabled. |
| 51 | + |
| 52 | +## Soundness Caveats |
| 53 | + |
| 54 | +### CBMC backend |
| 55 | +Kani uses [CBMC](https://github.com/diffblue/cbmc) as its verification backend. |
| 56 | +CBMC is a mature tool but, like any complex software, may contain bugs. Kani |
| 57 | +pins a specific CBMC version and runs CBMC's regression suite as part of its CI. |
| 58 | + |
| 59 | +### Bounded verification |
| 60 | +Kani performs bounded model checking. Loops are unwound up to a configurable |
| 61 | +bound (`--default-unwind`). If the bound is insufficient, Kani emits an |
| 62 | +unwinding assertion failure. Verification results are sound only if all |
| 63 | +unwinding assertions pass. |
| 64 | + |
| 65 | +### Floating-point arithmetic |
| 66 | +CBMC's floating-point reasoning uses bit-precise IEEE 754 semantics for the SAT |
| 67 | +backend. Results are sound for standard floating-point operations. However, some |
| 68 | +platform-specific floating-point behavior (e.g., x87 extended precision) may |
| 69 | +differ from the verification model. |
| 70 | + |
| 71 | +### Object size limits |
| 72 | +CBMC represents pointers with a fixed number of object bits (default: 16, |
| 73 | +configurable via `--cbmc-args --object-bits N`). Programs that allocate more |
| 74 | +objects than `2^N` may exhibit incorrect wrapping behavior. This is a known |
| 75 | +limitation tracked in [#1150](https://github.com/model-checking/kani/issues/1150). |
| 76 | + |
| 77 | +### Function pointers |
| 78 | +By default, unresolved function pointers are modeled as nondeterministic calls |
| 79 | +to any function with a compatible signature. This is sound but may be imprecise |
| 80 | +(reporting spurious failures). An unstable `--restrict-vtable` flag limits |
| 81 | +dispatch targets based on vtable analysis, but this feature is experimental and |
| 82 | +may be imprecise in the other direction (missing valid targets). |
| 83 | + |
| 84 | +## Reporting Soundness Issues |
| 85 | + |
| 86 | +If you believe Kani has failed to detect a genuine issue (false negative), |
| 87 | +please file a bug report with the `[F] Soundness` label at the |
| 88 | +[soundness issues tracker](https://github.com/model-checking/kani/issues?q=label%3A%22%5BF%5D+Soundness%22). |
0 commit comments