SilverSight/docs/reviews/avmisa_audit_report.md

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	Q16_16 type definition + arithmetic kernels
Step.lean	AVM instruction semantics
State.lean	Machine state (stack, locals, pc)
Run.lean	Fuel-bounded execution loop

---

§1 — Arithmetic Vulnerability Surfaces

V1. Multiplication Intermediate Overflow ⚠️ CRITICAL

Definition:

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:

   #eval (q16MaxRaw * q16MaxRaw) -- should be ≤ 2^62, fits Int64
   

---

V2. Division Intermediate Overflow ⚠️ CRITICAL

Definition:

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:

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:

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:

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.