From 138b3b97f629f8165ff35bb0ee4d017ba787da94 Mon Sep 17 00:00:00 2001 From: Allaun Silverfox <28494262+allaunthefox@users.noreply.github.com> Date: Thu, 2 Jul 2026 03:37:23 +0200 Subject: [PATCH] Remove avmisa_audit_report.md --- docs/reviews/avmisa_audit_report.md | 218 ---------------------------- 1 file changed, 218 deletions(-) delete mode 100644 docs/reviews/avmisa_audit_report.md diff --git a/docs/reviews/avmisa_audit_report.md b/docs/reviews/avmisa_audit_report.md deleted file mode 100644 index 4df7e133..00000000 --- a/docs/reviews/avmisa_audit_report.md +++ /dev/null @@ -1,218 +0,0 @@ -# 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.