commit 6dd91fa69d98bf078cf11ec505c236699993bd5d
parent 191611b72312b0990f0e4488c2c61ce47bcd1c3a
Author: Jared Tobin <jared@jtobin.io>
Date: Thu, 26 Feb 2026 17:22:02 +0400
fix: improve secret_pointee handling and add tests
Address reviewer feedback:
- Handle register-offset addressing modes (BaseReg, BaseRegShift,
BaseRegExtend) for secret_pointee, not just BaseImm
- Require KindPtr and Public taint for isSecretDataPointer, so
non-pointer arithmetic invalidates the secret pointee property
- Add comprehensive tests:
- Load through secret_pointee with immediate offset
- Load through secret_pointee with register offset
- secret takes precedence over secret_pointee
- Non-pointer arithmetic (mul) invalidates secret_pointee
- Pointer arithmetic (add #imm) preserves secret_pointee
Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com>
Diffstat:
2 files changed, 111 insertions(+), 1 deletion(-)
diff --git a/lib/Audit/AArch64/Taint.hs b/lib/Audit/AArch64/Taint.hs
@@ -618,8 +618,13 @@ isPublicPointer r st =
-- | Check if a register is a pointer to secret data.
-- Loads through such pointers produce Secret values.
+-- Requires the register to be a Public pointer with ProvSecretData provenance.
+-- If arithmetic mutates it to a scalar, it's no longer a valid secret pointer.
isSecretDataPointer :: Reg -> TaintState -> Bool
-isSecretDataPointer r st = getProvenance r st == ProvSecretData
+isSecretDataPointer r st =
+ getTaint r st == Public &&
+ getKind r st == KindPtr &&
+ getProvenance r st == ProvSecretData
-- | Set a heap slot for a (base, offset) pair.
setHeapSlot :: Reg -> Int -> Taint -> Provenance -> RegKind -> TaintState
@@ -845,6 +850,16 @@ loadFromStack dst addr st = case addr of
BaseImm base imm
| isPublicPointer base st ->
setTaintLoadHeapSlot dst base (fromInteger imm) st
+ -- Secret data pointer with register offset: [base, xM] variants
+ BaseReg base _idx
+ | isSecretDataPointer base st ->
+ setTaintProvKind dst Secret ProvUnknown KindScalar st
+ BaseRegShift base _idx _shift
+ | isSecretDataPointer base st ->
+ setTaintProvKind dst Secret ProvUnknown KindScalar st
+ BaseRegExtend base _idx _ext
+ | isSecretDataPointer base st ->
+ setTaintProvKind dst Secret ProvUnknown KindScalar st
-- Other loads: read from coarse heap bucket
_ -> setTaintLoadHeap dst st
diff --git a/test/Main.hs b/test/Main.hs
@@ -15,6 +15,15 @@ import qualified Data.Text as T
import Test.Tasty
import Test.Tasty.HUnit
+-- | Check if a violation reason is secret (not unknown).
+isSecretViolation :: ViolationReason -> Bool
+isSecretViolation r = case r of
+ SecretBase _ -> True
+ SecretIndex _ -> True
+ UnknownBase _ -> False
+ UnknownIndex _ -> False
+ NonConstOffset -> True
+
main :: IO ()
main = defaultMain $ testGroup "ppad-auditor" [
parserTests
@@ -898,6 +907,92 @@ taintConfigTests = testGroup "TaintConfig" [
st = seedArgs policy initTaintState
assertEqual "X0 is secret" Secret (getTaint X0 st)
+ , testCase "secret_pointee load with imm offset produces Secret" $ do
+ -- x0 is pointer to secret data; ldr through it produces Secret
+ let src = T.unlines
+ [ "_foo:"
+ , " ldr x1, [x0, #8]" -- Load through secret_pointee
+ , " ldr x2, [x21, x1]" -- Use as index -> violation
+ , " ret"
+ ]
+ cfg = TaintConfig (Map.singleton "_foo"
+ (ArgPolicy Set.empty Set.empty (Set.singleton X0)
+ Set.empty Set.empty)) True
+ case auditWithConfig cfg "test" src of
+ Left e -> assertFailure $ "parse failed: " ++ show e
+ Right ar -> do
+ assertEqual "one violation" 1 (length (arViolations ar))
+ case arViolations ar of
+ [v] -> assertEqual "secret index" (SecretIndex X1) (vReason v)
+ _ -> assertFailure "expected exactly one violation"
+
+ , testCase "secret_pointee load with reg offset produces Secret" $ do
+ -- x0 is pointer to secret data; ldr [x0, x1] produces Secret
+ -- x1 is unknown, so we get: unknown index x1 + secret index x2
+ let src = T.unlines
+ [ "_foo:"
+ , " ldr x2, [x0, x1]" -- Load through secret_pointee with reg idx
+ , " ldr x3, [x21, x2]" -- Use as index -> violation
+ , " ret"
+ ]
+ cfg = TaintConfig (Map.singleton "_foo"
+ (ArgPolicy Set.empty Set.empty (Set.singleton X0)
+ Set.empty Set.empty)) True
+ case auditWithConfig cfg "test" src of
+ Left e -> assertFailure $ "parse failed: " ++ show e
+ Right ar -> do
+ -- Two violations: unknown x1 index, secret x2 index
+ assertEqual "two violations" 2 (length (arViolations ar))
+ let reasons = map vReason (arViolations ar)
+ assertBool "has secret index x2" (SecretIndex X2 `elem` reasons)
+
+ , testCase "secret takes precedence over secret_pointee" $ do
+ -- If both secret and secret_pointee, secret wins (scalar, not pointer)
+ let policy = ArgPolicy (Set.singleton X0) Set.empty (Set.singleton X0)
+ Set.empty Set.empty
+ st = seedArgs policy initTaintState
+ assertEqual "X0 is secret" Secret (getTaint X0 st)
+ -- Secret scalar is not a secret_pointee (provenance is ProvUnknown)
+ assertEqual "X0 provenance" ProvUnknown (getProvenance X0 st)
+
+ , testCase "non-pointer arithmetic invalidates secret_pointee" $ do
+ -- mul produces KindScalar, so x0 is no longer a valid pointer
+ -- Loads through it go to coarse heap bucket (Unknown), not Secret
+ let src = T.unlines
+ [ "_foo:"
+ , " mul x0, x0, x1" -- Multiply -> KindScalar
+ , " ldr x2, [x0, #0]" -- Load from heap bucket (not secret)
+ , " ldr x3, [x21, x2]" -- Use as index -> unknown, not secret
+ , " ret"
+ ]
+ cfg = TaintConfig (Map.singleton "_foo"
+ (ArgPolicy Set.empty Set.empty (Set.singleton X0)
+ Set.empty Set.empty)) True
+ case auditWithConfig cfg "test" src of
+ Left e -> assertFailure $ "parse failed: " ++ show e
+ Right ar ->
+ -- No secret violations (x2 is Unknown from heap, not Secret)
+ assertEqual "no secret violations" 0
+ (length $ filter isSecretViolation (map vReason (arViolations ar)))
+
+ , testCase "pointer arithmetic preserves secret_pointee" $ do
+ -- add with immediate keeps KindPtr, so x0 is still secret_pointee
+ let src = T.unlines
+ [ "_foo:"
+ , " add x0, x0, #8" -- Pointer arithmetic -> KindPtr
+ , " ldr x1, [x0, #0]" -- Load through secret_pointee -> Secret
+ , " ldr x2, [x21, x1]" -- Use as index -> secret violation
+ , " ret"
+ ]
+ cfg = TaintConfig (Map.singleton "_foo"
+ (ArgPolicy Set.empty Set.empty (Set.singleton X0)
+ Set.empty Set.empty)) True
+ case auditWithConfig cfg "test" src of
+ Left e -> assertFailure $ "parse failed: " ++ show e
+ Right ar -> do
+ assertEqual "one secret violation" 1
+ (length $ filter isSecretViolation (map vReason (arViolations ar)))
+
, testCase "secret arg causes violation on indexed access" $ do
let src = T.unlines
[ "_mul_wnaf:"
