47 lines
2 KiB
Markdown
47 lines
2 KiB
Markdown
# Bounded symbolic soundness contract
|
|
|
|
## Model relation
|
|
|
|
Let `C_k` be the concrete executions within the configured loop/call bound and
|
|
let `E_k` be fold's encoded executions. For an over-approximated encoding, the
|
|
required relation is `C_k ⊆ E_k`: every bounded concrete execution has an
|
|
encoded counterpart, while the encoding may admit additional executions.
|
|
|
|
Typed bit-vector operations are exact where the source width and signedness are
|
|
known. Unknown calls, unsupported nodes and types, loop havoc, and timeouts are
|
|
not exact; they must be recorded in the encoding precision context.
|
|
|
|
## UNSAT results
|
|
|
|
If `E_k ∧ H` is UNSAT, no execution in `C_k` can satisfy hazard `H`. This is the
|
|
safe direction of proof under over-approximation and is used for bounded
|
|
unreachability and invariant checks.
|
|
|
|
The conclusion remains bounded: it says nothing about executions beyond the
|
|
configured loop/call bound or translation units and binaries outside the scan.
|
|
|
|
## SAT results
|
|
|
|
If `E_k ∧ H` is SAT, the model is a candidate hazard witness. It corresponds to
|
|
a bounded concrete execution only when the encoding that supports the query is
|
|
exact. A SAT model from an over-approximated encoding may be spurious.
|
|
|
|
Accordingly, the confidence contract is:
|
|
|
|
- `proved`: an exact bounded model established the property (SAT for a hazard
|
|
witness, or UNSAT for a negated invariant);
|
|
- `latent`: the intra-procedural model is exact, but a caller/environment
|
|
obligation remains undischarged;
|
|
- `heuristic`: an unsupported or over-approximated operation contributes to the
|
|
result;
|
|
- `concrete-witness`: a sanitizer/runtime failure was strictly correlated with
|
|
the predicted hazard.
|
|
|
|
Detectors must propagate the sink-time encoding precision into evidence and
|
|
must not label an over-approximated SAT result `proved`.
|
|
|
|
## Exact fragment
|
|
|
|
For loop-free, call-free functions whose used operations and types are fully
|
|
encoded, the bounded model can be exact. Exactness is a per-query property, not
|
|
a blanket property of every integer-only function or every 64-bit encoding.
|