From 0e5ed5694eb97971771bcca841d0f0a6a316fa9d Mon Sep 17 00:00:00 2001 From: Allaun Silverfox <28494262+allaunthefox@users.noreply.github.com> Date: Thu, 2 Jul 2026 03:37:19 +0200 Subject: [PATCH] Archive avmisa_audit_report.md --- .../docs/reviews/avmisa_audit_report.md | 218 ++++++++++++++++++ 1 file changed, 218 insertions(+) create mode 100644 archive/2026-07-02/docs/reviews/avmisa_audit_report.md diff --git a/archive/2026-07-02/docs/reviews/avmisa_audit_report.md b/archive/2026-07-02/docs/reviews/avmisa_audit_report.md new file mode 100644 index 00000000..4df7e133 --- /dev/null +++ b/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.