auditor

commit 58c63e037805555270aeedcd49dcb19673287f05
parent ecca408f0f28a71cfdccfd40c6e0dd32e84a539c
Author: Jared Tobin <jared@jtobin.io>
Date:   Tue, 10 Feb 2026 14:05:23 +0400

fix: invalidate stack map when SP is modified

Clears the stack slot taint map when SP changes to prevent unsound
taint tracking with stale offsets. Handles:

- add/sub with SP as destination
- Pre-indexed stores: [sp, #imm]! (modifies SP after access)
- Post-indexed loads: [sp], #imm (modifies SP after access)

Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com>

Diffstat:
M
lib/Audit/AArch64/Taint.hs
 | 
37
++++++++++++++++++++++++++++++-------

1 file changed, 30 insertions(+), 7 deletions(-)
diff --git a/lib/Audit/AArch64/Taint.hs b/lib/Audit/AArch64/Taint.hs
@@ -118,8 +118,9 @@ transfer instr st = case instr of
   Movn dst _ _ -> setTaint dst Public st  -- Immediate is public
 
   -- Arithmetic: result is join of operand taints
-  Add dst r1 op -> setTaint dst (join2 (getTaint r1 st) (operandTaint op st)) st
-  Sub dst r1 op -> setTaint dst (join2 (getTaint r1 st) (operandTaint op st)) st
+  -- Clear stack map if SP is modified (offsets become stale)
+  Add dst r1 op -> updateWithSpCheck dst (join2 (getTaint r1 st) (operandTaint op st)) st
+  Sub dst r1 op -> updateWithSpCheck dst (join2 (getTaint r1 st) (operandTaint op st)) st
   Adds dst r1 op -> setTaint dst (join2 (getTaint r1 st) (operandTaint op st)) st
   Subs dst r1 op -> setTaint dst (join2 (getTaint r1 st) (operandTaint op st)) st
   Adc dst r1 r2 -> setTaint dst (join2 (getTaint r1 st) (getTaint r2 st)) st
@@ -238,15 +239,29 @@ setTaintLoadStack dst offset st
 setStackTaint :: Int -> Taint -> TaintState -> TaintState
 setStackTaint offset t st = st { tsStack = IM.insert offset t (tsStack st) }
 
+-- | Clear all stack slot taints (when SP is modified).
+clearStackMap :: TaintState -> TaintState
+clearStackMap st = st { tsStack = IM.empty }
+
+-- | Update register taint, clearing stack map if dst is SP.
+updateWithSpCheck :: Reg -> Taint -> TaintState -> TaintState
+updateWithSpCheck dst t st
+  | dst == SP = clearStackMap (setTaint dst t st)
+  | otherwise = setTaint dst t st
+
 -- | Track a store to stack if address is [sp, #imm].
+-- Pre-indexed addressing modifies SP, invalidating the stack map.
 storeToStack :: Reg -> AddrMode -> TaintState -> TaintState
 storeToStack src addr st = case addr of
   BaseImm SP imm -> setStackTaint (fromInteger imm) (getTaint src st) st
-  PreIndex SP imm -> setStackTaint (fromInteger imm) (getTaint src st) st
+  PreIndex SP imm ->
+    -- Store first, then clear (SP changes after access)
+    clearStackMap (setStackTaint (fromInteger imm) (getTaint src st) st)
   _ -> st  -- Non-SP stores don't affect stack tracking
 
 -- | Track a store pair to stack if address is [sp, #imm].
 -- Stores src1 at offset and src2 at offset+8.
+-- Pre-indexed addressing modifies SP, invalidating the stack map.
 storePairToStack :: Reg -> Reg -> AddrMode -> TaintState -> TaintState
 storePairToStack src1 src2 addr st = case addr of
   BaseImm SP imm ->
@@ -254,33 +269,41 @@ storePairToStack src1 src2 addr st = case addr of
     in  setStackTaint off (getTaint src1 st)
           (setStackTaint (off + 8) (getTaint src2 st) st)
   PreIndex SP imm ->
+    -- Store first, then clear (SP changes after access)
     let off = fromInteger imm
-    in  setStackTaint off (getTaint src1 st)
-          (setStackTaint (off + 8) (getTaint src2 st) st)
+        st' = setStackTaint off (getTaint src1 st)
+                (setStackTaint (off + 8) (getTaint src2 st) st)
+    in  clearStackMap st'
   _ -> st
 
 -- | Load from memory, handling special cases:
 -- - [sp, #imm]: restore tracked stack slot taint
 -- - [r, symbol@GOTPAGEOFF]: GOT entry load, result is Public (address)
 -- - Other: Unknown unless dst is a public root
+-- Post-indexed addressing modifies SP, invalidating the stack map.
 loadFromStack :: Reg -> AddrMode -> TaintState -> TaintState
 loadFromStack dst addr st = case addr of
   BaseImm SP imm -> setTaintLoadStack dst (fromInteger imm) st
-  PostIndex SP imm -> setTaintLoadStack dst (fromInteger imm) st
+  PostIndex SP imm ->
+    -- Load first, then clear (SP changes after access)
+    clearStackMap (setTaintLoadStack dst (fromInteger imm) st)
   BaseSymbol _ _ -> setTaint dst Public st  -- GOT/PLT entry -> address
   Literal _ -> setTaint dst Public st  -- PC-relative literal -> address
   _ -> setTaintLoad dst st  -- Other loads use default behavior
 
 -- | Load pair from stack if address is [sp, #imm].
 -- Loads dst1 from offset and dst2 from offset+8.
+-- Post-indexed addressing modifies SP, invalidating the stack map.
 loadPairFromStack :: Reg -> Reg -> AddrMode -> TaintState -> TaintState
 loadPairFromStack dst1 dst2 addr st = case addr of
   BaseImm SP imm ->
     let off = fromInteger imm
     in  setTaintLoadStack dst1 off (setTaintLoadStack dst2 (off + 8) st)
   PostIndex SP imm ->
+    -- Load first, then clear (SP changes after access)
     let off = fromInteger imm
-    in  setTaintLoadStack dst1 off (setTaintLoadStack dst2 (off + 8) st)
+        st' = setTaintLoadStack dst1 off (setTaintLoadStack dst2 (off + 8) st)
+    in  clearStackMap st'
   _ -> setTaintLoad dst1 (setTaintLoad dst2 st)
 
 -- | Get taint of an operand.