commit f1f3facd8d49e27fc1f2d90ed222d42025838043
parent 3ce10429d8b217ce743eaf8823961afa536a9aba
Author: Jared Tobin <jared@jtobin.io>
Date: Thu, 26 Feb 2026 17:12:42 +0400
feat: add secret_pointee policy for pointer-to-secret semantics
Adds support for marking registers as pointers to secret data, where
the pointer address is public but loads through it produce Secret
taint. This models closure pointers whose payloads contain secrets.
Changes:
- Add ProvSecretData to Provenance type
- Add apSecretPointee field to ArgPolicy
- Add "secret_pointee" JSON key for taint configs
- Update load handling to produce Secret when base has ProvSecretData
- joinProvenance: ProvSecretData dominates ProvPublic
Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com>
Diffstat:
3 files changed, 73 insertions(+), 37 deletions(-)
diff --git a/lib/Audit/AArch64/Taint.hs b/lib/Audit/AArch64/Taint.hs
@@ -178,21 +178,28 @@ initTaintStateWith assumeStgPublic = TaintState
-- | Seed argument registers and STG stack slots according to policy.
-- Secret registers are marked Secret with ProvUnknown.
-- Public registers are marked Public with ProvPublic.
--- If a register/slot appears in both lists, secret takes precedence.
+-- Secret pointee registers are marked Public/ProvSecretData/KindPtr.
+-- If a register/slot appears in multiple lists, secret takes precedence.
seedArgs :: ArgPolicy -> TaintState -> TaintState
seedArgs policy st =
- let -- Apply public first, then secret (so secret wins on overlap)
+ let -- Apply public first, then secret pointee, then secret (so secret wins)
st1 = Set.foldr markPublic st (apPublic policy)
- st2 = Set.foldr markSecret st1 (apSecret policy)
+ st2 = Set.foldr markSecretPointee st1 (apSecretPointee policy)
+ st3 = Set.foldr markSecret st2 (apSecret policy)
-- Seed STG stack slots
- st3 = Set.foldr markStgPublic st2 (apStgPublic policy)
- st4 = Set.foldr markStgSecret st3 (apStgSecret policy)
- in st4
+ st4 = Set.foldr markStgPublic st3 (apStgPublic policy)
+ st5 = Set.foldr markStgSecret st4 (apStgSecret policy)
+ in st5
where
markPublic r s = s
{ tsRegs = Map.insert r Public (tsRegs s)
, tsProv = Map.insert r ProvPublic (tsProv s)
}
+ markSecretPointee r s = s
+ { tsRegs = Map.insert r Public (tsRegs s)
+ , tsProv = Map.insert r ProvSecretData (tsProv s)
+ , tsKind = Map.insert r KindPtr (tsKind s)
+ }
markSecret r s = s
{ tsRegs = Map.insert r Secret (tsRegs s)
, tsProv = Map.insert r ProvUnknown (tsProv s)
@@ -609,6 +616,11 @@ isPublicPointer :: Reg -> TaintState -> Bool
isPublicPointer r st =
getKind r st == KindPtr && getProvenance r st == ProvPublic
+-- | Check if a register is a pointer to secret data.
+-- Loads through such pointers produce Secret values.
+isSecretDataPointer :: Reg -> TaintState -> Bool
+isSecretDataPointer r st = getProvenance r st == ProvSecretData
+
-- | Set a heap slot for a (base, offset) pair.
setHeapSlot :: Reg -> Int -> Taint -> Provenance -> RegKind -> TaintState
-> TaintState
@@ -825,6 +837,10 @@ loadFromStack dst addr st = case addr of
setTaintProv dst Public ProvPublic st -- GOT/PLT entry -> address
Literal _ ->
setTaintProv dst Public ProvPublic st -- PC-relative literal -> address
+ -- Secret data pointer: [base, #imm] where base points to secret data
+ BaseImm base _imm
+ | isSecretDataPointer base st ->
+ setTaintProvKind dst Secret ProvUnknown KindScalar st
-- Refined heap slot: [base, #imm] where base is a public pointer
BaseImm base imm
| isPublicPointer base st ->
@@ -867,6 +883,11 @@ loadPairFromStack dst1 dst2 addr st = case addr of
delta = negate (fromInteger imm)
st' = setTaintLoadStgStack dst1 off (setTaintLoadStgStack dst2 (off+8) st)
in shiftStgStackMap delta st'
+ -- Secret data pointer: [base, #imm] where base points to secret data
+ BaseImm base _imm
+ | isSecretDataPointer base st ->
+ setTaintProvKind dst1 Secret ProvUnknown KindScalar
+ (setTaintProvKind dst2 Secret ProvUnknown KindScalar st)
-- Refined heap slot: [base, #imm] where base is a public pointer
BaseImm base imm
| isPublicPointer base st ->
diff --git a/lib/Audit/AArch64/Types.hs b/lib/Audit/AArch64/Types.hs
@@ -333,16 +333,22 @@ joinTaint _ _ = Unknown -- Public+Unknown or Unknown+Unknown
-- | Provenance: tracks whether a value derives from known-public sources.
-- Used to upgrade Unknown taint to Public when provenance can prove safety.
data Provenance
- = ProvPublic -- ^ Derived from public root or constant
- | ProvUnknown -- ^ Unknown origin (e.g., loaded from memory)
+ = ProvPublic -- ^ Derived from public root or constant
+ | ProvUnknown -- ^ Unknown origin (e.g., loaded from memory)
+ | ProvSecretData -- ^ Pointer to secret data (loads through it produce Secret)
deriving (Eq, Ord, Show, Generic, NFData)
instance ToJSON Provenance
--- | Join provenance: only ProvPublic if both are ProvPublic.
+-- | Join provenance: ProvPublic only if both are ProvPublic.
+-- ProvSecretData dominates ProvPublic (conservative: might point to secrets).
+-- ProvUnknown dominates everything (can't prove anything).
joinProvenance :: Provenance -> Provenance -> Provenance
-joinProvenance ProvPublic ProvPublic = ProvPublic
-joinProvenance _ _ = ProvUnknown
+joinProvenance ProvPublic ProvPublic = ProvPublic
+joinProvenance ProvSecretData ProvSecretData = ProvSecretData
+joinProvenance ProvSecretData ProvPublic = ProvSecretData
+joinProvenance ProvPublic ProvSecretData = ProvSecretData
+joinProvenance _ _ = ProvUnknown
-- | Register kind: distinguishes pointers from scalars.
-- Used to restrict provenance upgrades to pointer-kind registers only.
@@ -401,20 +407,28 @@ instance ToJSON Violation where
-- | Per-function argument taint policy.
-- Specifies which registers and STG stack slots should be seeded.
data ArgPolicy = ArgPolicy
- { apSecret :: !(Set Reg) -- ^ Registers to mark as Secret
- , apPublic :: !(Set Reg) -- ^ Registers to mark as Public
- , apStgSecret :: !(Set Int) -- ^ STG stack offsets (x20-relative) to mark Secret
- , apStgPublic :: !(Set Int) -- ^ STG stack offsets (x20-relative) to mark Public
+ { apSecret :: !(Set Reg)
+ -- ^ Registers to mark as Secret (scalar values)
+ , apPublic :: !(Set Reg)
+ -- ^ Registers to mark as Public
+ , apSecretPointee :: !(Set Reg)
+ -- ^ Registers that are pointers to secret data.
+ -- The pointer itself is public, but loads through it produce Secret values.
+ , apStgSecret :: !(Set Int)
+ -- ^ STG stack offsets (x20-relative) to mark Secret
+ , apStgPublic :: !(Set Int)
+ -- ^ STG stack offsets (x20-relative) to mark Public
} deriving (Eq, Show)
-- | Empty argument policy (no overrides).
emptyArgPolicy :: ArgPolicy
-emptyArgPolicy = ArgPolicy Set.empty Set.empty Set.empty Set.empty
+emptyArgPolicy = ArgPolicy Set.empty Set.empty Set.empty Set.empty Set.empty
instance FromJSON ArgPolicy where
parseJSON = withObject "ArgPolicy" $ \o -> do
secretTexts <- o .:? "secret"
publicTexts <- o .:? "public"
+ secretPointeeTexts <- o .:? "secret_pointee"
stgSecretInts <- o .:? "stg_secret"
stgPublicInts <- o .:? "stg_public"
let parseRegs :: Maybe [Text] -> Either Text (Set Reg)
@@ -428,10 +442,11 @@ instance FromJSON ArgPolicy where
parseInts :: Maybe [Int] -> Set Int
parseInts Nothing = Set.empty
parseInts (Just is) = Set.fromList is
- case (parseRegs secretTexts, parseRegs publicTexts) of
- (Left e, _) -> fail (T.unpack e)
- (_, Left e) -> fail (T.unpack e)
- (Right s, Right p) -> pure $ ArgPolicy s p
+ case (parseRegs secretTexts, parseRegs publicTexts, parseRegs secretPointeeTexts) of
+ (Left e, _, _) -> fail (T.unpack e)
+ (_, Left e, _) -> fail (T.unpack e)
+ (_, _, Left e) -> fail (T.unpack e)
+ (Right s, Right p, Right sp) -> pure $ ArgPolicy s p sp
(parseInts stgSecretInts) (parseInts stgPublicInts)
-- | Taint configuration: maps function symbols to argument policies.
diff --git a/test/Main.hs b/test/Main.hs
@@ -537,7 +537,7 @@ auditTests = testGroup "Audit" [
, " ret"
]
cfg = TaintConfig (Map.singleton "_foo"
- (ArgPolicy (Set.singleton X0) Set.empty Set.empty Set.empty)) True
+ (ArgPolicy (Set.singleton X0) Set.empty Set.empty Set.empty Set.empty)) True
case auditWithConfig cfg "test" src of
Left e -> assertFailure $ "parse failed: " ++ show e
Right ar -> do
@@ -561,7 +561,7 @@ auditTests = testGroup "Audit" [
, " ret"
]
cfg = TaintConfig (Map.singleton "_foo"
- (ArgPolicy (Set.singleton X0) Set.empty Set.empty Set.empty)) True
+ (ArgPolicy (Set.singleton X0) Set.empty Set.empty Set.empty Set.empty)) True
case auditWithConfig cfg "test" src of
Left e -> assertFailure $ "parse failed: " ++ show e
Right ar -> do
@@ -586,7 +586,7 @@ auditTests = testGroup "Audit" [
, " ret"
]
cfg = TaintConfig (Map.singleton "_foo"
- (ArgPolicy (Set.singleton X0) Set.empty Set.empty Set.empty)) True
+ (ArgPolicy (Set.singleton X0) Set.empty Set.empty Set.empty Set.empty)) True
case auditWithConfig cfg "test" src of
Left e -> assertFailure $ "parse failed: " ++ show e
Right ar -> assertEqual "no violations" 0 (length (arViolations ar))
@@ -604,7 +604,7 @@ auditTests = testGroup "Audit" [
, " ret"
]
cfg = TaintConfig (Map.singleton "_foo"
- (ArgPolicy (Set.singleton X0) Set.empty Set.empty Set.empty)) True
+ (ArgPolicy (Set.singleton X0) Set.empty Set.empty Set.empty Set.empty)) True
case auditWithConfig cfg "test" src of
Left e -> assertFailure $ "parse failed: " ++ show e
Right ar -> do
@@ -626,7 +626,7 @@ auditTests = testGroup "Audit" [
, " ret"
]
cfg = TaintConfig (Map.singleton "_foo"
- (ArgPolicy (Set.singleton X0) Set.empty Set.empty Set.empty)) True
+ (ArgPolicy (Set.singleton X0) Set.empty Set.empty Set.empty Set.empty)) True
case auditWithConfig cfg "test" src of
Left e -> assertFailure $ "parse failed: " ++ show e
Right ar -> do
@@ -884,17 +884,17 @@ taintConfigTests = testGroup "TaintConfig" [
Right _ -> assertFailure "should have failed on invalid register"
, testCase "seedArgs marks secret" $ do
- let policy = ArgPolicy (Set.singleton X0) Set.empty Set.empty Set.empty
+ let policy = ArgPolicy (Set.singleton X0) Set.empty Set.empty Set.empty Set.empty
st = seedArgs policy initTaintState
assertEqual "X0 is secret" Secret (getTaint X0 st)
, testCase "seedArgs marks public" $ do
- let policy = ArgPolicy Set.empty (Set.singleton X0) Set.empty Set.empty
+ let policy = ArgPolicy Set.empty (Set.singleton X0) Set.empty Set.empty Set.empty
st = seedArgs policy initTaintState
assertEqual "X0 is public" Public (getTaint X0 st)
, testCase "secret takes precedence over public" $ do
- let policy = ArgPolicy (Set.singleton X0) (Set.singleton X0) Set.empty Set.empty
+ let policy = ArgPolicy (Set.singleton X0) (Set.singleton X0) Set.empty Set.empty Set.empty
st = seedArgs policy initTaintState
assertEqual "X0 is secret" Secret (getTaint X0 st)
@@ -905,7 +905,7 @@ taintConfigTests = testGroup "TaintConfig" [
, " ret"
]
cfg = TaintConfig (Map.singleton "_mul_wnaf"
- (ArgPolicy (Set.singleton X0) Set.empty Set.empty Set.empty)) True
+ (ArgPolicy (Set.singleton X0) Set.empty Set.empty Set.empty Set.empty)) True
case auditWithConfig cfg "test" src of
Left e -> assertFailure $ "parse failed: " ++ show e
Right ar -> do
@@ -923,7 +923,7 @@ taintConfigTests = testGroup "TaintConfig" [
, " ret"
]
cfg = TaintConfig (Map.singleton "_foo"
- (ArgPolicy Set.empty (Set.singleton X0) Set.empty Set.empty)) True
+ (ArgPolicy Set.empty (Set.singleton X0) Set.empty Set.empty Set.empty)) True
case auditWithConfig cfg "test" src of
Left e -> assertFailure $ "parse failed: " ++ show e
Right ar -> assertEqual "no violations" 0 (length (arViolations ar))
@@ -935,7 +935,7 @@ taintConfigTests = testGroup "TaintConfig" [
, " ret"
]
cfg = TaintConfig (Map.singleton "_mul_wnaf"
- (ArgPolicy (Set.singleton X0) Set.empty Set.empty Set.empty)) True
+ (ArgPolicy (Set.singleton X0) Set.empty Set.empty Set.empty Set.empty)) True
case auditInterProcWithConfig cfg "test" src of
Left e -> assertFailure $ "parse failed: " ++ show e
Right ar -> do
@@ -971,7 +971,7 @@ taintConfigTests = testGroup "TaintConfig" [
, " ret"
]
cfg = TaintConfig (Map.singleton "_foo"
- (ArgPolicy Set.empty Set.empty (Set.singleton 8) Set.empty)) True
+ (ArgPolicy Set.empty Set.empty Set.empty (Set.singleton 8) Set.empty)) True
case auditWithConfig cfg "test" src of
Left e -> assertFailure $ "parse failed: " ++ show e
Right ar -> do
@@ -991,7 +991,7 @@ taintConfigTests = testGroup "TaintConfig" [
, " ret"
]
cfg = TaintConfig (Map.singleton "_foo"
- (ArgPolicy Set.empty Set.empty Set.empty (Set.singleton 16))) True
+ (ArgPolicy Set.empty Set.empty Set.empty Set.empty (Set.singleton 16))) True
case auditWithConfig cfg "test" src of
Left e -> assertFailure $ "parse failed: " ++ show e
Right ar -> assertEqual "no violations" 0 (length (arViolations ar))
@@ -1005,7 +1005,7 @@ taintConfigTests = testGroup "TaintConfig" [
, " ret"
]
cfg = TaintConfig (Map.singleton "_foo"
- (ArgPolicy Set.empty Set.empty
+ (ArgPolicy Set.empty Set.empty Set.empty
(Set.singleton 8) (Set.singleton 8))) True
case auditWithConfig cfg "test" src of
Left e -> assertFailure $ "parse failed: " ++ show e
@@ -1029,7 +1029,7 @@ taintConfigTests = testGroup "TaintConfig" [
, " ret"
]
cfg = TaintConfig (Map.singleton "_foo"
- (ArgPolicy Set.empty Set.empty (Set.singleton 8) Set.empty)) True
+ (ArgPolicy Set.empty Set.empty Set.empty (Set.singleton 8) Set.empty)) True
case auditWithConfig cfg "test" src of
Left e -> assertFailure $ "parse failed: " ++ show e
Right ar -> do
@@ -1051,7 +1051,7 @@ taintConfigTests = testGroup "TaintConfig" [
, " ret"
]
cfg = TaintConfig (Map.singleton "_foo"
- (ArgPolicy Set.empty Set.empty (Set.singleton 24) Set.empty)) True
+ (ArgPolicy Set.empty Set.empty Set.empty (Set.singleton 24) Set.empty)) True
case auditWithConfig cfg "test" src of
Left e -> assertFailure $ "parse failed: " ++ show e
Right ar -> do
@@ -1074,7 +1074,7 @@ taintConfigTests = testGroup "TaintConfig" [
, " ret"
]
cfg = TaintConfig (Map.singleton "_foo"
- (ArgPolicy Set.empty Set.empty (Set.singleton 8) Set.empty)) True
+ (ArgPolicy Set.empty Set.empty Set.empty (Set.singleton 8) Set.empty)) True
case auditWithConfig cfg "test" src of
Left e -> assertFailure $ "parse failed: " ++ show e
Right ar -> do
