Archive avmisa_audit_report.md

archive/2026-07-02/docs/reviews/avmisa_audit_report.md

@@ -0,0 +1,218 @@
+# AVMIsa Manual Math Audit — Vulnerability Report
+
+This report walks through every arithmetic path in the AVM ISA step-by-step,
+identifies how each can go wrong, and proposes concrete mitigations.
+
+---
+
+## Source Files Under Audit
+
+| File | Role |
+|------|------|
+| [FixedPoint.lean](file:///home/allaun/SilverSight/Core/SilverSight/FixedPoint.lean) | Q16_16 type definition + arithmetic kernels |
+| [Step.lean](file:///home/allaun/SilverSight/formal/SilverSight/AVMIsa/Step.lean) | AVM instruction semantics |
+| [State.lean](file:///home/allaun/SilverSight/formal/SilverSight/AVMIsa/State.lean) | Machine state (stack, locals, pc) |
+| [Run.lean](file:///home/allaun/SilverSight/formal/SilverSight/AVMIsa/Run.lean) | Fuel-bounded execution loop |
+
+---
+
+## §1 — Arithmetic Vulnerability Surfaces
+
+### V1. Multiplication Intermediate Overflow ⚠️ CRITICAL
+
+**Definition:**
+```lean
+def mul (a b : Q16_16) : Q16_16 := ofRawInt ((a.toInt * b.toInt) / q16Scale)
+```
+
+**The problem:** `a.toInt` and `b.toInt` are both in $[-2^{31}, 2^{31}-1]$.
+Their product can reach $2^{62}$, which is fine in Lean (arbitrary-precision `Int`),
+but **any backend using 32-bit integers will silently overflow**.
+
+**Worked example:**
+- $a = 32767.0$ (raw $2147418112$), $b = 2.0$ (raw $131072$)
+- Intermediate: $2147418112 \times 131072 = 2.81 \times 10^{17}$ → overflows `int32`
+- Even `int64` handles this, but a 32-bit C/Verilog backend will produce garbage
+
+**Mitigation:**
+1. **Backend spec rule:** All AVM backends MUST use ≥ 64-bit intermediate storage for `mul` and `div`
+2. **Lean-side:** Add a `#eval` witness confirming the worst-case product fits in `Int64`:
+   ```lean
+   #eval (q16MaxRaw * q16MaxRaw) -- should be ≤ 2^62, fits Int64
+   ```
+
+---
+
+### V2. Division Intermediate Overflow ⚠️ CRITICAL
+
+**Definition:**
+```lean
+def div (a b : Q16_16) : Q16_16 :=
+  if b.toInt = 0 then infinity else ofRawInt ((a.toInt * q16Scale) / b.toInt)
+```
+
+**The problem:** `a.toInt * 65536` can reach $2^{31} \times 2^{16} = 2^{47}$,
+which overflows `int32` but fits `int64`.
+
+**Worked example:**
+- $a = \text{maxVal}$ (raw $2147483647$), $b = 1.0$ (raw $65536$)
+- Intermediate: $2147483647 \times 65536 = 1.407 \times 10^{14}$ → overflows `int32`
+
+**Mitigation:** Same as V1 — mandate 64-bit intermediates for all backends.
+
+---
+
+### V3. Division by Zero Sentinel ⚠️ MEDIUM
+
+**Definition:** `div(a, 0)` returns `infinity` (which is `maxVal = 2147483647`).
+
+**The problem:** This is a **silent sentinel** — the caller cannot distinguish
+"the result was legitimately very large" from "division by zero occurred."
+In a bidirectional encoding pipeline, this could silently corrupt a DNA sequence
+if a zero denominator arises from a degenerate AST.
+
+**Mitigation options (pick one):**
+1. **Add a `StepError.divisionByZero`** error variant and make `divSatQ16` return
+   `Outcome.err StepError.divisionByZero` instead of a sentinel value
+2. **Add a `Prim.isDivSafe`** instruction that pushes `true` if TOS ≠ 0, allowing
+   programs to guard division explicitly
+3. **Accept the sentinel** but document it as a backend invariant and add a
+   `#eval` witness confirming `div maxVal zero = maxVal`
+
+> [!IMPORTANT]
+> Option 1 is the most rigid but changes the `Outcome` contract.
+> Option 2 preserves totality while giving programs the ability to guard.
+
+---
+
+### V4. Rounding Direction Mismatch ⚠️ CRITICAL (Cross-Platform)
+
+**Lean's integer division:** Truncation toward zero (same as C99 `/`).
+- $-7 / 2 = -3$ (truncates toward zero)
+
+**Python's `//` operator:** Floor division (rounds toward $-\infty$).
+- $-7 // 2 = -4$ (floors)
+
+**Impact on `mul`:**
+- $a = -1$ (raw $-65536$), $b = 0.5$ (raw $32768$)
+- Lean: $(-65536 \times 32768) / 65536 = -2147483648 / 65536 = -32768$ (truncation)
+- Python: $(-65536 \times 32768) // 65536 = -32768$ (same here, but...)
+
+- $a$ raw $= -3$, $b$ raw $= 2$:
+- Lean: $(-3 \times 2) / 65536 = -6 / 65536 = 0$ (truncates toward zero)
+- Python: $(-6) // 65536 = -1$ (floors toward $-\infty$)
+- **Result differs by 1 LSB** → DNA sequence divergence
+
+**Mitigation:**
+1. **BioSight Python shim MUST use `int(x / y)` (truncation) instead of `x // y` (floor)**
+   for all Q16_16 operations
+2. Add a cross-platform conformance test: compute `mul(ofRawInt(-3), ofRawInt(2))`
+   in both Lean and Python and assert identical raw values
+
+---
+
+### V5. Saturation Asymmetry ⚠️ LOW
+
+**Range:** $[-2147483648, 2147483647]$ — the negative range has 1 more value than
+the positive range. This means:
+- `neg(minVal)` = `ofRawInt(2147483648)` → saturates to `maxVal` ($2147483647$)
+- So `neg(neg(minVal)) ≠ minVal` — negation is not an involution at the boundary
+
+**Impact:** For bidirectional encoding, if a DNA base encodes `minVal` and the
+decoder negates twice, it will get `maxVal - 1` instead. This is a 1-LSB error
+at the extreme boundary.
+
+**Mitigation:**
+1. Document this as a known boundary: the extreme negative value $-2^{31}$ is
+   outside the invertible range
+2. Restrict the encoding domain to $[-2^{31}+1, 2^{31}-1]$ so negation is always invertible
+
+---
+
+### V6. Comparison Signedness ⚠️ LOW
+
+**`ltQ16` in Step.lean:**
+```lean
+let res := y.toInt < x.toInt
+```
+
+This uses `Int` comparison which is correct for signed Q16_16. However, if a
+backend implements this using unsigned comparison on the raw bits, large negative
+values would appear positive and comparisons would be inverted.
+
+**Mitigation:** Backend spec must state: "All Q16_16 comparisons use **signed**
+integer comparison on the raw representation."
+
+---
+
+## §2 — Execution & Memory Vulnerability Surfaces
+
+### V7. Unbounded Stack Growth ⚠️ MEDIUM
+
+**State definition:**
+```lean
+structure State where
+  pc : Nat
+  stack : List AnyVal
+  locals : List (Option AnyVal)
+  halted : Bool
+```
+
+The stack is an unbounded `List`. A malicious or buggy program could push
+indefinitely (e.g., `push; jump 0` loop), consuming unbounded memory before
+fuel runs out.
+
+**Worst case:** With fuel $= N$, the stack can grow to depth $N$ values
+($N \times 12$ bytes for the tag+payload). At fuel $= 2^{20}$, that's ~12 MB.
+
+**Mitigation:**
+1. Add a `maxStackDepth : Nat` field to `State` and check it on every `push`
+2. Add a new `StepError.stackOverflow` variant
+3. Or: accept fuel as the implicit bound and document the relationship
+   $\text{max\_stack} \leq \text{fuel}$
+
+---
+
+### V8. Local Frame Silent No-Op on Out-of-Bounds Store ⚠️ MEDIUM
+
+**`setLocal` definition:**
+```lean
+def setLocal (s : State) (i : Nat) (v : AnyVal) : State :=
+  if i < s.locals.length then
+    { s with locals := s.locals.set i (some v) }
+  else
+    s  -- silent no-op!
+```
+
+If `i ≥ locals.length`, the store is silently dropped. The program continues
+with stale data, which could lead to incorrect DNA encodings without any error signal.
+
+**Mitigation:**
+1. Return `Outcome.err StepError.missingLocal` on out-of-bounds store (matching
+   the behavior of `load`, which already returns `missingLocal`)
+2. Or: pre-allocate the local frame to a fixed size at program start
+
+---
+
+## §3 — Summary Matrix
+
+| ID | Surface | Severity | Status |
+|----|---------|----------|--------|
+| V1 | mul intermediate overflow (32-bit backends) | 🔴 Critical | Open |
+| V2 | div intermediate overflow (32-bit backends) | 🔴 Critical | Open |
+| V3 | div-by-zero returns silent sentinel | 🟡 Medium | Open |
+| V4 | Rounding direction mismatch (Lean vs Python) | 🔴 Critical | Open |
+| V5 | Negation non-involution at minVal boundary | 🟢 Low | Documented |
+| V6 | Comparison signedness in backends | 🟢 Low | Documented |
+| V7 | Unbounded stack growth | 🟡 Medium | Open |
+| V8 | Silent no-op on out-of-bounds store | 🟡 Medium | Open |
+
+## §4 — Recommended Priority Order
+
+1. **V4 (Rounding)** — Fix the Python shim first. This is the most likely source
+   of real DNA sequence divergence between Lean and Python today.
+2. **V1/V2 (Overflow)** — Add 64-bit mandate to backend spec + `#eval` witnesses.
+3. **V8 (Silent store)** — Change `setLocal` to error on out-of-bounds.
+4. **V3 (Div-by-zero)** — Add `isDivSafe` guard primitive or error variant.
+5. **V7 (Stack growth)** — Add stack depth limit or accept fuel as bound.
+6. **V5/V6** — Document as known boundaries.