811aab5254
- H1: &&/|| short-circuit not forked → 30-40% null-deref FP reduction - H3: Rust IR incomplete (Member, Conditional, signedness, path) - 7 recommended fixes ordered by effort/impact - Precision gaps mapped per detector family
167 lines
7.7 KiB
Markdown
167 lines
7.7 KiB
Markdown
## Z3 Symbolic Encoder Robustness Audit
|
|
|
|
**Scope:** Every file in `src/symbolic/*.cpp` and `include/fold/symbolic/*.hpp` (31 files)
|
|
**Date:** 2026-05-27
|
|
|
|
---
|
|
|
|
### 1. PATH PREDICATE PRECISION
|
|
|
|
#### 1.1 If/Else Forking — ADEQUATE with gaps
|
|
|
|
The walker (`src/detect/security_walker.cpp`, `walkIf()`) correctly forks the `SymbolicEnv` into `then_env` and `else_env` at every `IfStmt`, setting path predicates `path && cond` and `path && !cond` respectively. A `z3::solver::push()`/`pop()` pair wraps each arm so branch-local constraints don't leak.
|
|
|
|
**Phi-merge at join points** is conditionally applied: when both arms produce identical values for all live variables, the env is directly reused (cheap merge). Otherwise, phi variables are created with constraint `phi == ite(cond, then_v, else_v)`, and the path predicate is restored to pre-if.
|
|
|
|
**Gaps:**
|
|
|
|
| Gap | Location | Severity |
|
|
|-----|----------|----------|
|
|
| **Short-circuit `&&`/`||` not path-forked** | `encoder.cpp` `encodeBinary`, `BO_LAnd`/`BO_LOr` | HIGH |
|
|
| **WalkIf short-circuit handling incomplete** | `walkIf` uses `encodeConditionWithShortCircuit` for condition only | MEDIUM |
|
|
|
|
The `BO_LAnd` and `BO_LOr` arms fall through to simple `coerceToBool(lhs) && coerceToBool(rhs)` — treating them as eager boolean expressions. This is a **known FP class (Class D)** documented at `encoder.cpp` line ~1082: *"3 of 4 yams null-deref FPs are `(p != nullptr && p->m)` or `(p == nullptr || *p != ...)`"*.
|
|
|
|
#### 1.2 Ternaries — ADEQUATE
|
|
|
|
`encodeExpr` handles `ConditionalOperator` by forking two child envs with `path && cond` / `path && !cond`, encoding each arm, then combining via `z3::ite()`. Special handling for `assert(x)` macro patterns.
|
|
|
|
#### 1.3 Switch Statements — PARTIAL
|
|
|
|
`walkSwitch` encodes the condition but does NOT refine path predicates per case. Each case body runs against the same undifferentiated path.
|
|
|
|
#### 1.4 Loop Unrolling — ADEQUATE
|
|
|
|
Loop unrolling depth defaults to 5 (`SolverBudget::loop_unroll`). Canonical `for` loops are detected with tight interval ranges. Loop invariant inference is implemented but **unused** (`z3::fixedpoint` → `spdlog::debug` only).
|
|
|
|
---
|
|
|
|
### 2. TYPE THREADING
|
|
|
|
| Area | Status |
|
|
|------|--------|
|
|
| Source bit-widths | ADEQUATE — `sourceWidth()` returns bit-width, `coerceToExactBv` materializes |
|
|
| Signedness | ADEQUATE for Clang, **PARTIAL for Rust** — `int_signed` field exists but ignored |
|
|
| Struct fields | PARTIAL — field offset tracked, but field type info not threaded to observers |
|
|
| Union members | **NOT HANDLED** — no overlapping-storage constraints |
|
|
| Array elements | ADEQUATE — `z3::select` with known-length propagation |
|
|
|
|
**Rust signedness gap (HIGH):** `rust_ir_encoder.cpp` hard-codes `true` for signedness in all `onBinaryArith`/`onDivision` calls. The `RustExprNode` struct has `int_signed` but it is unused.
|
|
|
|
---
|
|
|
|
### 3. INTERPROCEDURAL HANDLING
|
|
|
|
**Direct calls (ADEQUATE):** Summary lookup, malloc/free tracking, stdlib sink recognition, string-length propagation, M20 non-null marking.
|
|
|
|
**Indirect calls / virtual dispatch (NOT HANDLED — HIGH):** `calleeName()` returns empty for indirect calls. Falls through to `OverApproximated` fresh-unknown return. Virtual dispatch through C++ vtables is completely opaque.
|
|
|
|
---
|
|
|
|
### 4. MEMORY MODEL
|
|
|
|
**HeapModel tracks:** regions (base, size, freed flag), derived pointers, OOB checking, use-after-free checking, concrete alias disambiguation via allocation IDs.
|
|
|
|
**Gaps:**
|
|
- No symbolic alias analysis — pointers tracked as BV-64 values only
|
|
- Stack arrays not in HeapModel — excluded from OOB/UAF queries
|
|
- Field access values are `freshUnknown` — no type/width preservation
|
|
- `mergeFrom` loses path-sensitivity for freed — crude boolean OR at phi-joins
|
|
|
|
---
|
|
|
|
### 5. RUST IR COMPLETENESS
|
|
|
|
| Kind | Handled? | Notes |
|
|
|------|----------|-------|
|
|
| IntegerLiteral, BoolLiteral, NullPtr, DeclRef | Yes | |
|
|
| BinaryOp, Deref, ArraySubscript, UnaryOp | Yes | |
|
|
| AddrOf, Cast, Call(transmute) | Yes | Pass-through or special-case |
|
|
| Call(other) | PARTIAL | Args only; no summaries |
|
|
| **Member** | **NO** | Absent from switch |
|
|
| **HeapNew/HeapDelete** | **NO** | Absent |
|
|
| **StringLiteral** | **NO** | Absent |
|
|
| **Conditional** | **NO** | No path forking |
|
|
| **ConstructorCall** | **NO** | No modeling |
|
|
| Default fallthrough | Returns BV-0 | |
|
|
|
|
Critical: No path predicate accumulation in Rust IR encoder — `path` starts as `true` and is never updated. All comparison operators use unsigned semantics despite `int_signed` being available.
|
|
|
|
---
|
|
|
|
### 6. Z3 QUERY CONSTRUCTION
|
|
|
|
- **Logic:** QF_BV ✓
|
|
- **Timeouts:** Per-query 2000ms (configurable) ✓
|
|
- **Caching:** LRU ExprCache per Z3 expression hash (4096 entries, thread-safe) ✓
|
|
- **Path predicates:** Can grow unbounded — no simplification or bounding applied
|
|
|
|
---
|
|
|
|
## PRECISION GAP SUMMARY
|
|
|
|
### HIGH severity — Directly causes false positives
|
|
|
|
| # | Gap | FP Class | Detectors | Estimated FP Impact |
|
|
|---|-----|----------|-----------|---------------------|
|
|
| H1 | `&&`/`||` short-circuit not forked | `if (p && p->field)` | null-deref | 30-40% of null-deref FPs |
|
|
| H2 | Indirect/virtual calls not resolved | Opaque callsites | All detectors | Misses findings |
|
|
| H3 | Rust IR incomplete (Member, Conditional, signedness, path) | All Rust ops | All Rust detectors | Near-total precision loss |
|
|
|
|
### MEDIUM severity
|
|
|
|
| # | Gap | Detectors |
|
|
|---|-----|-----------|
|
|
| M1 | Switch case path predicates not refined | null-deref, oob, dead-branch |
|
|
| M2 | Loop invariant inference unused | All post-loop detectors |
|
|
| M3 | Field type info not threaded to observers | int-overflow, sign-conversion |
|
|
| M4 | Union members not modeled | All memory-safety detectors |
|
|
| M5 | HeapModel mergeFrom loses freed path-sensitivity | UAF (future) |
|
|
| M6 | Rust comparisons always unsigned | All Rust detectors |
|
|
|
|
### LOW severity
|
|
|
|
| # | Gap |
|
|
|---|-----|
|
|
| L1 | Path predicate unbounded growth (perf) |
|
|
| L2 | ExprCache cleared per-function (perf) |
|
|
| L3 | Rust AdrOf/Cast pass-through (type info loss) |
|
|
| L4 | Stack arrays not in HeapModel |
|
|
|
|
---
|
|
|
|
## RECOMMENDED FIXES ORDERED BY ROI
|
|
|
|
### Fix 1: Fork path predicate for `&&`/`||` in encoder (H1)
|
|
**Effort:** S (~50 lines) | **ROI:** Highest
|
|
**Files:** `src/symbolic/encoder.cpp`, `encodeBinary`
|
|
**Approach:** In `BO_LAnd`/`BO_LOr` arms, fork env like `ConditionalOperator`: `lhs_env` with `path && lhs`, `rhs_env` with `path && !lhs && rhs`, encode RHS only in `rhs_env`.
|
|
|
|
### Fix 2: Wire Rust signedness through observer hooks (H3)
|
|
**Effort:** S (~10 lines) | **ROI:** Very high for Rust
|
|
**Files:** `src/symbolic/rust_ir_encoder.cpp`
|
|
**Approach:** Pass `node->int_signed` instead of hard-coded `true`.
|
|
|
|
### Fix 3: Add Rust `Member` + Conditional encoding (H3)
|
|
**Effort:** M (~80 lines) | **ROI:** Moderate
|
|
**Files:** `src/symbolic/rust_ir_encoder.cpp`
|
|
**Approach:** Add `Member` case (base encoding + `onPointerDerefIr`), add `Conditional` case with path-forking.
|
|
|
|
### Fix 4: Wire loop invariant results (M2)
|
|
**Effort:** S (~30 lines) | **ROI:** Moderate
|
|
**Files:** `src/symbolic/loop_invariant.cpp`, `src/detect/security_walker.cpp`
|
|
**Approach:** Use `invariant->invariant_expr` in `unrollLoop` to constrain widened range.
|
|
|
|
### Fix 5: Per-case path predicates in switch (M1)
|
|
**Effort:** M (~60 lines) | **ROI:** Moderate
|
|
**Files:** `src/detect/security_walker.cpp`
|
|
**Approach:** For each `CaseStmt`, add `switch_expr == case_val` to path predicate.
|
|
|
|
### Fix 6: Thread field type info through `onMemberAccess` (M3)
|
|
**Effort:** M (~40 lines) | **ROI:** Low-Moderate
|
|
**Files:** `include/fold/symbolic/safety_observer.hpp`, `src/symbolic/encoder.cpp`
|
|
|
|
### Fix 7: Indirect call / virtual dispatch resolution (H2)
|
|
**Effort:** L | **ROI:** High for C++ OO codebases
|
|
**Files:** `src/symbolic/encoder.cpp`
|
|
**Approach:** Enumerate possible targets via clang VTable analysis, model as `ite` over typeid choices.
|