From 37ea14842af9df8357be3c98a1420366af9621a7 Mon Sep 17 00:00:00 2001 From: allaun Date: Sun, 28 Jun 2026 00:11:18 -0500 Subject: [PATCH] fix(avm): AVMIsa vulnerability mitigations V3/V7/V8 + overflow/rounding witnesses MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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 --- formal/SilverSight/AVMIsa/Run.lean | 37 ++++++++++++++ formal/SilverSight/AVMIsa/State.lean | 11 ++++- formal/SilverSight/AVMIsa/Step.lean | 72 +++++++++++++++++++++------- 3 files changed, 103 insertions(+), 17 deletions(-) diff --git a/formal/SilverSight/AVMIsa/Run.lean b/formal/SilverSight/AVMIsa/Run.lean index de0e5d63..10d75969 100644 --- a/formal/SilverSight/AVMIsa/Run.lean +++ b/formal/SilverSight/AVMIsa/Run.lean @@ -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 diff --git a/formal/SilverSight/AVMIsa/State.lean b/formal/SilverSight/AVMIsa/State.lean index 11895427..8c9d93e4 100644 --- a/formal/SilverSight/AVMIsa/State.lean +++ b/formal/SilverSight/AVMIsa/State.lean @@ -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) } diff --git a/formal/SilverSight/AVMIsa/Step.lean b/formal/SilverSight/AVMIsa/Step.lean index a5e47820..ae9a498a 100644 --- a/formal/SilverSight/AVMIsa/Step.lean +++ b/formal/SilverSight/AVMIsa/Step.lean @@ -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 }