mirror of
https://github.com/allaunthefox/SilverSight.git
synced 2026-07-31 01:25:21 +00:00
Remove avmisa_audit_report.md
This commit is contained in:
Allaun Silverfox
parent
0e5ed5694e
commit
138b3b97f6
1 changed files with 0 additions and 218 deletions
|
|
@ -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.
|
||||
Loading…
Add table
Reference in a new issue