allaun/SilverSight
1
0
Fork 0
mirror of https://github.com/allaunthefox/SilverSight.git synced 2026-07-31 01:25:21 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions

fix(avm): AVMIsa vulnerability mitigations V3/V7/V8 + overflow/rounding witnesses

Browse source 
V3 (Critical — Division-by-zero sentinel):
  - Add StepError.divisionByZero variant
  - Guard q16_div with explicit zero check (Outcome.err on zero divisor)

V7 (Medium — Unbounded stack):
  - Add maxStackDepth := 1024 constant
  - Refactor push1 to return Outcome (stack bounds check)
  - Add push1_unchecked for proof compatibility
  - Add push1_ok_of_lt theorem
  - Guard Instr.push and Instr.dup with stack depth checks

V8 (Medium — Silent store):
  - Add setLocal? to State.lean returning Option State
  - Wire store instruction to propagate missingLocal on OOB
  - Preserve backward-compatible setLocal for TypeSafety proofs

V1/V2 (Critical — Intermediate overflow):
  - Add #eval witnesses proving worst-case intermediates fit Int64
  - Backend spec mandate: all AVM backends MUST use >= 64-bit storage

V4 (Critical — Rounding direction):
  - Add #eval witnesses documenting Euclidean division semantics
  - Note: Lean ediv matches Python // for positive divisors only
This commit is contained in:
allaun 2026-06-28 00:11:18 -05:00
parent cb50581eef
commit 37ea14842a
3 changed files with 103 additions and 17 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

37
formal/SilverSight/AVMIsa/Run.lean
View file

@ -79,4 +79,41 @@ def canaryState : State :=
#eval run 8 canaryDiv canaryState
#eval run 8 canaryLt canaryState
-- ─────────────────────────────────────────────────────────────────────────────
-- §V1/V2 Overflow safety witnesses
-- ─────────────────────────────────────────────────────────────────────────────
/-- V1 witness: worst-case mul intermediate fits Int64.
maxRaw * maxRaw = 2147483647² = 4611686014132420609, which is < 2^63. -/
#eval do
let maxRaw : Int := 2147483647
let prod := maxRaw * maxRaw
let fits := prod < (1 <<< 63 : Int)
IO.println s!"V1 mul worst-case intermediate: {prod}, fits Int64: {fits}"
/-- V2 witness: worst-case div intermediate fits Int64.
maxRaw * 65536 = 2147483647 * 65536 = 140737488289792, which is < 2^63. -/
#eval do
let maxRaw : Int := 2147483647
let prod := maxRaw * 65536
let fits := prod < (1 <<< 63 : Int)
IO.println s!"V2 div worst-case intermediate: {prod}, fits Int64: {fits}"
-- ─────────────────────────────────────────────────────────────────────────────
-- §V4 Rounding direction conformance witness
-- ─────────────────────────────────────────────────────────────────────────────
/-- V4 witness: Lean Int.div is EUCLIDEAN (remainder always ≥ 0).
-6 / 65536 = -1 (not 0 as in C99 truncation, not -1 as in floor [same here]).
For POSITIVE divisors, Euclidean matches Python's //.
For NEGATIVE divisors, they diverge:
Lean ediv: 65536 / (-3) = -21845 (rem 1, r ≥ 0)
Python //: 65536 // (-3) = -21846 (rem -2, floor)
Python backends MUST use _ediv() for q16_div when b may be negative. -/
#eval do
let r1 := (-6 : Int) / (65536 : Int)
IO.println s!"V4a: (-6) / 65536 = {r1} (Euclidean, expect -1)"
let r2 := (65536 : Int) / (-3 : Int)
IO.println s!"V4b: 65536 / (-3) = {r2} (Euclidean, expect -21845)"
end SilverSight.AVMIsa

11
formal/SilverSight/AVMIsa/State.lean
View file

@ -21,7 +21,16 @@ deriving Inhabited, Repr
def getLocal? (s : State) (i : Nat) : Option AnyVal :=
s.locals.getD i none
/-- Safe locals set (no-op when out of bounds). -/
/-- Safe locals set.
V8 mitigation: returns `none` on out-of-bounds instead of silently
dropping the store. The step function maps this to StepError.missingLocal. -/
def setLocal? (s : State) (i : Nat) (v : AnyVal) : Option State :=
if i < s.locals.length then
some { s with locals := s.locals.set i (some v) }
else
none
/-- Backward-compatible wrapper (used by TypeSafety proofs). -/
def setLocal (s : State) (i : Nat) (v : AnyVal) : State :=
if i < s.locals.length then
{ s with locals := s.locals.set i (some v) }

72
formal/SilverSight/AVMIsa/Step.lean
View file

@ -10,6 +10,8 @@ inductive StepError : Type where
| typeMismatch
| invalidJump
| missingLocal
| divisionByZero -- V3: explicit div-by-zero (no silent sentinel)
| stackOverflow -- V7: stack depth exceeded maxStackDepth
deriving Inhabited, DecidableEq, BEq, Repr
/-- Outcome type for AVM execution.
@ -27,10 +29,31 @@ def pop1 (s : State) : Outcome (AnyVal × State) :=
| [] => Outcome.err StepError.stackUnderflow
| x :: xs => Outcome.ok (x, { s with stack := xs })
/-- Push one element onto stack. -/
def push1 (s : State) (v : AnyVal) : State :=
/-- Maximum stack depth.
V7 mitigation: bounds stack growth to prevent runaway push loops from
consuming unbounded memory. 1024 values × ~12 bytes each = ~12 KB max.
Programs needing deeper stacks should use locals or restructure. -/
def maxStackDepth : Nat := 1024
/-- Unchecked push (used in proofs for structural reasoning). -/
def push1_unchecked (s : State) (v : AnyVal) : State :=
{ s with stack := v :: s.stack }
/-- Push one element onto stack, checking depth bound.
V7 mitigation: returns `Outcome.err stackOverflow` if limit is exceeded. -/
def push1 (s : State) (v : AnyVal) : Outcome State :=
if s.stack.length ≥ maxStackDepth then
Outcome.err StepError.stackOverflow
else
Outcome.ok (push1_unchecked s v)
/-- When stack is below limit, push1 succeeds and equals push1_unchecked. -/
theorem push1_ok_of_lt {s : State} {v : AnyVal}
(h : s.stack.length < maxStackDepth) :
push1 s v = Outcome.ok (push1_unchecked s v) := by
unfold push1
rw [if_neg (by omega)]
/-- Evaluate a primitive.
NOTE: This v1 skeleton implements only a small subset. Extend strictly by
@ -44,7 +67,7 @@ def evalPrim (p : Prim) (s : State) : Outcome State :=
| Outcome.ok (v, s1) =>
match v with
| ⟨AvmTy.bool, AvmVal.b x⟩ =>
Outcome.ok (push1 s1 ⟨AvmTy.bool, AvmVal.b (!x)⟩)
push1 s1 ⟨AvmTy.bool, AvmVal.b (!x)⟩
| _ => Outcome.err StepError.typeMismatch
| Prim.and =>
match pop1 s with
@ -55,7 +78,7 @@ def evalPrim (p : Prim) (s : State) : Outcome State :=
| Outcome.ok (v2, s2) =>
match v1, v2 with
| ⟨AvmTy.bool, AvmVal.b b1⟩, ⟨AvmTy.bool, AvmVal.b b2⟩ =>
Outcome.ok (push1 s2 ⟨AvmTy.bool, AvmVal.b (b2 && b1)⟩)
push1 s2 ⟨AvmTy.bool, AvmVal.b (b2 && b1)⟩
| _, _ => Outcome.err StepError.typeMismatch
| Prim.or =>
match pop1 s with
@ -66,7 +89,7 @@ def evalPrim (p : Prim) (s : State) : Outcome State :=
| Outcome.ok (v2, s2) =>
match v1, v2 with
| ⟨AvmTy.bool, AvmVal.b b1⟩, ⟨AvmTy.bool, AvmVal.b b2⟩ =>
Outcome.ok (push1 s2 ⟨AvmTy.bool, AvmVal.b (b2 || b1)⟩)
push1 s2 ⟨AvmTy.bool, AvmVal.b (b2 || b1)⟩
| _, _ => Outcome.err StepError.typeMismatch
| Prim.addSatQ0 =>
match pop1 s with
@ -77,7 +100,7 @@ def evalPrim (p : Prim) (s : State) : Outcome State :=
| Outcome.ok (v2, s2) =>
match v1, v2 with
| ⟨AvmTy.q0_16, AvmVal.q0 x⟩, ⟨AvmTy.q0_16, AvmVal.q0 y⟩ =>
Outcome.ok (push1 s2 ⟨AvmTy.q0_16, AvmVal.q0 (SilverSight.Q0_16.add y x)⟩)
push1 s2 ⟨AvmTy.q0_16, AvmVal.q0 (SilverSight.Q0_16.add y x)⟩
| _, _ => Outcome.err StepError.typeMismatch
| Prim.subSatQ0 =>
match pop1 s with
@ -88,7 +111,7 @@ def evalPrim (p : Prim) (s : State) : Outcome State :=
| Outcome.ok (v2, s2) =>
match v1, v2 with
| ⟨AvmTy.q0_16, AvmVal.q0 x⟩, ⟨AvmTy.q0_16, AvmVal.q0 y⟩ =>
Outcome.ok (push1 s2 ⟨AvmTy.q0_16, AvmVal.q0 (SilverSight.Q0_16.sub y x)⟩)
push1 s2 ⟨AvmTy.q0_16, AvmVal.q0 (SilverSight.Q0_16.sub y x)⟩
| _, _ => Outcome.err StepError.typeMismatch
| Prim.addSatQ16 =>
match pop1 s with
@ -99,7 +122,7 @@ def evalPrim (p : Prim) (s : State) : Outcome State :=
| Outcome.ok (v2, s2) =>
match v1, v2 with
| ⟨AvmTy.q16_16, AvmVal.q16 x⟩, ⟨AvmTy.q16_16, AvmVal.q16 y⟩ =>
Outcome.ok (push1 s2 ⟨AvmTy.q16_16, AvmVal.q16 (SilverSight.Q16_16.add y x)⟩)
push1 s2 ⟨AvmTy.q16_16, AvmVal.q16 (SilverSight.Q16_16.add y x)⟩
| _, _ => Outcome.err StepError.typeMismatch
| Prim.subSatQ16 =>
match pop1 s with
@ -110,7 +133,7 @@ def evalPrim (p : Prim) (s : State) : Outcome State :=
| Outcome.ok (v2, s2) =>
match v1, v2 with
| ⟨AvmTy.q16_16, AvmVal.q16 x⟩, ⟨AvmTy.q16_16, AvmVal.q16 y⟩ =>
Outcome.ok (push1 s2 ⟨AvmTy.q16_16, AvmVal.q16 (SilverSight.Q16_16.sub y x)⟩)
push1 s2 ⟨AvmTy.q16_16, AvmVal.q16 (SilverSight.Q16_16.sub y x)⟩
| _, _ => Outcome.err StepError.typeMismatch
| Prim.mulSatQ16 =>
match pop1 s with
@ -121,9 +144,10 @@ def evalPrim (p : Prim) (s : State) : Outcome State :=
| Outcome.ok (v2, s2) =>
match v1, v2 with
| ⟨AvmTy.q16_16, AvmVal.q16 x⟩, ⟨AvmTy.q16_16, AvmVal.q16 y⟩ =>
Outcome.ok (push1 s2 ⟨AvmTy.q16_16, AvmVal.q16 (SilverSight.Q16_16.mul y x)⟩)
push1 s2 ⟨AvmTy.q16_16, AvmVal.q16 (SilverSight.Q16_16.mul y x)⟩
| _, _ => Outcome.err StepError.typeMismatch
| Prim.divSatQ16 =>
-- V3 mitigation: explicit division-by-zero error
match pop1 s with
| Outcome.err e => Outcome.err e
| Outcome.ok (v1, s1) =>
@ -132,7 +156,10 @@ def evalPrim (p : Prim) (s : State) : Outcome State :=
| Outcome.ok (v2, s2) =>
match v1, v2 with
| ⟨AvmTy.q16_16, AvmVal.q16 x⟩, ⟨AvmTy.q16_16, AvmVal.q16 y⟩ =>
Outcome.ok (push1 s2 ⟨AvmTy.q16_16, AvmVal.q16 (SilverSight.Q16_16.div y x)⟩)
if x.toInt = 0 then
Outcome.err StepError.divisionByZero
else
push1 s2 ⟨AvmTy.q16_16, AvmVal.q16 (SilverSight.Q16_16.div y x)⟩
| _, _ => Outcome.err StepError.typeMismatch
| Prim.ltQ16 =>
match pop1 s with
@ -144,7 +171,7 @@ def evalPrim (p : Prim) (s : State) : Outcome State :=
match v1, v2 with
| ⟨AvmTy.q16_16, AvmVal.q16 x⟩, ⟨AvmTy.q16_16, AvmVal.q16 y⟩ =>
let res := y.toInt < x.toInt
Outcome.ok (push1 s2 ⟨AvmTy.bool, AvmVal.b res⟩)
push1 s2 ⟨AvmTy.bool, AvmVal.b res⟩
| _, _ => Outcome.err StepError.typeMismatch
| Prim.eqQ16 =>
match pop1 s with
@ -156,7 +183,7 @@ def evalPrim (p : Prim) (s : State) : Outcome State :=
match v1, v2 with
| ⟨AvmTy.q16_16, AvmVal.q16 x⟩, ⟨AvmTy.q16_16, AvmVal.q16 y⟩ =>
let res := y.val == x.val
Outcome.ok (push1 s2 ⟨AvmTy.bool, AvmVal.b res⟩)
push1 s2 ⟨AvmTy.bool, AvmVal.b res⟩
| _, _ => Outcome.err StepError.typeMismatch
/-- One-step execution.
@ -172,7 +199,12 @@ def step (program : List Instr) (s : State) : Outcome State :=
| some instr =>
match instr with
| Instr.halt => Outcome.ok { s with halted := true }
| Instr.push v => Outcome.ok { s with pc := s.pc + 1, stack := v :: s.stack }
| Instr.push v =>
-- V7: check stack depth on push
if s.stack.length ≥ maxStackDepth then
Outcome.err StepError.stackOverflow
else
Outcome.ok { s with pc := s.pc + 1, stack := v :: s.stack }
| Instr.pop =>
match pop1 s with
| Outcome.err e => Outcome.err e
@ -180,7 +212,12 @@ def step (program : List Instr) (s : State) : Outcome State :=
| Instr.dup =>
match s.stack with
| [] => Outcome.err StepError.stackUnderflow
| x :: xs => Outcome.ok { s with pc := s.pc + 1, stack := x :: x :: xs }
| x :: xs =>
-- V7: check stack depth on dup (grows stack by 1)
if s.stack.length ≥ maxStackDepth then
Outcome.err StepError.stackOverflow
else
Outcome.ok { s with pc := s.pc + 1, stack := x :: x :: xs }
| Instr.swap =>
match s.stack with
| a :: b :: xs => Outcome.ok { s with pc := s.pc + 1, stack := b :: a :: xs }
@ -192,7 +229,10 @@ def step (program : List Instr) (s : State) : Outcome State :=
| Instr.store i =>
match pop1 s with
| Outcome.err e => Outcome.err e
| Outcome.ok (v, s1) => Outcome.ok { (setLocal s1 i v) with pc := s.pc + 1 }
| Outcome.ok (v, s1) =>
match setLocal? s1 i v with
| some s2 => Outcome.ok { s2 with pc := s.pc + 1 }
| none => Outcome.err StepError.missingLocal
| Instr.jump target =>
if target < program.length then
Outcome.ok { s with pc := target }