auditor

An aarch64 constant-time memory access auditing tool.
git clone git://git.ppad.tech/auditor.git
Log | Files | Refs | README | LICENSE

commit 7ab24b4c9867f765cc2ff3a52dc42fb177750a0f
parent e427f099dbf1393289ecc30ae636afb62057d14c
Author: Jared Tobin <jared@jtobin.io>
Date:   Wed, 11 Feb 2026 22:25:09 +0400

feat: implement STG stack slot seeding via taint config (IMPL18)

Extend taint configuration to seed STG stack slots (x20-relative offsets)
as secret or public at function entry.

Changes:
- Add apStgSecret/apStgPublic fields to ArgPolicy for x20-relative offsets
- Update JSON parsing to accept stg_secret/stg_public arrays
- Extend seedArgs to apply STG stack slot seeding (secret wins on overlap)
- Add tests for JSON parsing and entry seeding behavior

Example config:
  {"_foo": {"secret": ["X23"], "stg_secret": [8, 152], "stg_public": [24]}}

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

Diffstat:
Mlib/Audit/AArch64/Taint.hs | 19++++++++++++++++---
Mlib/Audit/AArch64/Types.hs | 16++++++++++++----
Aplans/ARCH18.md | 43+++++++++++++++++++++++++++++++++++++++++++
Aplans/IMPL18.md | 40++++++++++++++++++++++++++++++++++++++++
Mtest/Main.hs | 98++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++---------
5 files changed, 198 insertions(+), 18 deletions(-)

diff --git a/lib/Audit/AArch64/Taint.hs b/lib/Audit/AArch64/Taint.hs @@ -160,16 +160,19 @@ initTaintState = TaintState , tsHeapSlots = Map.empty } --- | Seed argument registers according to policy. +-- | 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 appears in both lists, secret takes precedence. +-- If a register/slot appears in both lists, secret takes precedence. seedArgs :: ArgPolicy -> TaintState -> TaintState seedArgs policy st = let -- Apply public first, then secret (so secret wins on overlap) st1 = Set.foldr markPublic st (apPublic policy) st2 = Set.foldr markSecret st1 (apSecret policy) - in st2 + -- Seed STG stack slots + st3 = Set.foldr markStgPublic st2 (apStgPublic policy) + st4 = Set.foldr markStgSecret st3 (apStgSecret policy) + in st4 where markPublic r s = s { tsRegs = Map.insert r Public (tsRegs s) @@ -179,6 +182,16 @@ seedArgs policy st = { tsRegs = Map.insert r Secret (tsRegs s) , tsProv = Map.insert r ProvUnknown (tsProv s) } + markStgPublic off s = s + { tsStgStack = IM.insert off Public (tsStgStack s) + , tsStgStackProv = IM.insert off ProvPublic (tsStgStackProv s) + , tsStgStackKind = IM.insert off KindScalar (tsStgStackKind s) + } + markStgSecret off s = s + { tsStgStack = IM.insert off Secret (tsStgStack s) + , tsStgStackProv = IM.insert off ProvUnknown (tsStgStackProv s) + , tsStgStackKind = IM.insert off KindScalar (tsStgStackKind s) + } -- | Get the taint of a register. getTaint :: Reg -> TaintState -> Taint diff --git a/lib/Audit/AArch64/Types.hs b/lib/Audit/AArch64/Types.hs @@ -377,20 +377,24 @@ instance ToJSON Violation where ] -- | Per-function argument taint policy. --- Specifies which registers should be seeded as secret or public. +-- 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 + { 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 } deriving (Eq, Show) -- | Empty argument policy (no overrides). emptyArgPolicy :: ArgPolicy -emptyArgPolicy = ArgPolicy Set.empty Set.empty +emptyArgPolicy = ArgPolicy Set.empty Set.empty Set.empty Set.empty instance FromJSON ArgPolicy where parseJSON = withObject "ArgPolicy" $ \o -> do secretTexts <- o .:? "secret" publicTexts <- o .:? "public" + stgSecretInts <- o .:? "stg_secret" + stgPublicInts <- o .:? "stg_public" let parseRegs :: Maybe [Text] -> Either Text (Set Reg) parseRegs Nothing = Right Set.empty parseRegs (Just ts) = @@ -399,10 +403,14 @@ instance FromJSON ArgPolicy where in case bad of [] -> Right $ Set.fromList [r | (_, Just r) <- parsed] (b:_) -> Left $ "invalid register: " <> b + 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 + (parseInts stgSecretInts) (parseInts stgPublicInts) -- | Taint configuration: maps function symbols to argument policies. newtype TaintConfig = TaintConfig diff --git a/plans/ARCH18.md b/plans/ARCH18.md @@ -0,0 +1,43 @@ +# ARCH18: STG Stack Slot Seeding via Taint Config + +## Goal + +Allow taint configuration to seed STG stack slots (x20-relative offsets) +so secrets passed on the STG stack can be introduced into the analysis. + +## Scope + +- Extend taint config JSON schema with optional STG stack slot lists. +- Apply seeding at function entry alongside register seeding. + +## Config Model + +Example: + +{ + "_mul_wnaf_info": { + "secret": ["X23"], + "stg_secret": [8, 152], + "stg_public": [24] + } +} + +Semantics: + +- `stg_secret`: mark `tsStgStack` at those offsets as Secret. +- `stg_public`: mark `tsStgStack` at those offsets as Public. +- If an offset appears in both, secret wins. +- Offsets are signed integers (bytes) relative to `x20`. + +## Integration Points + +- Extend `ArgPolicy` to include STG stack slot lists. +- Update JSON parsing and validation. +- Update `seedArgs` (or add `seedStgStack`) to apply slot seeding. +- Apply seeding at function entry for config-aware runs. + +## Risks + +- Incorrect offsets cause false positives or missed findings. +- Stack slot tracking assumes `x20` is stable until modified; SP-like + clearing already handles `x20` updates. diff --git a/plans/IMPL18.md b/plans/IMPL18.md @@ -0,0 +1,40 @@ +# IMPL18: Implement STG Stack Slot Seeding + +## Summary + +Extend taint config and entry-state seeding to mark STG stack slots +(x20-relative offsets) as secret or public. + +## Steps + +1) Extend ArgPolicy +- Add `apStgSecret :: Set Int` and `apStgPublic :: Set Int`. +- Update JSON parsing to accept `stg_secret`/`stg_public` arrays. +- Validate offsets as integers. + +2) Seeding logic +- Add `seedStgStack :: ArgPolicy -> TaintState -> TaintState`. +- Apply public first, then secret (secret wins). +- Set taint/prov/kind appropriately for each slot: + - Secret -> Secret / ProvUnknown / KindUnknown (or KindScalar) + - Public -> Public / ProvPublic / KindPtr? (likely KindScalar) + +3) Entry-state integration +- Update `seedArgs` or entry seeding paths to include `seedStgStack`. +- Ensure both intra-proc and inter-proc config paths use it. + +4) Tests +- JSON parsing for `stg_secret`/`stg_public`. +- Entry seeding yields secret on load from `[x20, #imm]`. + +## Files to Touch + +- `lib/Audit/AArch64/Types.hs` +- `lib/Audit/AArch64/Taint.hs` +- `test/` + +## Validation + +- `cabal test` +- Run `mul_wnaf` with `stg_secret` offsets [8, 152] and expect + secret-indexed access to be flagged. diff --git a/test/Main.hs b/test/Main.hs @@ -492,7 +492,7 @@ auditTests = testGroup "Audit" [ , " ret" ] cfg = TaintConfig $ Map.singleton "_foo" - (ArgPolicy (Set.singleton X0) Set.empty) + (ArgPolicy (Set.singleton X0) Set.empty Set.empty Set.empty) case auditWithConfig cfg "test" src of Left e -> assertFailure $ "parse failed: " ++ show e Right ar -> do @@ -516,7 +516,7 @@ auditTests = testGroup "Audit" [ , " ret" ] cfg = TaintConfig $ Map.singleton "_foo" - (ArgPolicy (Set.singleton X0) Set.empty) + (ArgPolicy (Set.singleton X0) Set.empty Set.empty Set.empty) case auditWithConfig cfg "test" src of Left e -> assertFailure $ "parse failed: " ++ show e Right ar -> do @@ -541,7 +541,7 @@ auditTests = testGroup "Audit" [ , " ret" ] cfg = TaintConfig $ Map.singleton "_foo" - (ArgPolicy (Set.singleton X0) Set.empty) + (ArgPolicy (Set.singleton X0) Set.empty Set.empty Set.empty) case auditWithConfig cfg "test" src of Left e -> assertFailure $ "parse failed: " ++ show e Right ar -> assertEqual "no violations" 0 (length (arViolations ar)) @@ -559,7 +559,7 @@ auditTests = testGroup "Audit" [ , " ret" ] cfg = TaintConfig $ Map.singleton "_foo" - (ArgPolicy (Set.singleton X0) Set.empty) + (ArgPolicy (Set.singleton X0) Set.empty Set.empty Set.empty) case auditWithConfig cfg "test" src of Left e -> assertFailure $ "parse failed: " ++ show e Right ar -> do @@ -581,7 +581,7 @@ auditTests = testGroup "Audit" [ , " ret" ] cfg = TaintConfig $ Map.singleton "_foo" - (ArgPolicy (Set.singleton X0) Set.empty) + (ArgPolicy (Set.singleton X0) Set.empty Set.empty Set.empty) case auditWithConfig cfg "test" src of Left e -> assertFailure $ "parse failed: " ++ show e Right ar -> do @@ -782,17 +782,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 + let policy = ArgPolicy (Set.singleton X0) 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) + let policy = ArgPolicy Set.empty (Set.singleton X0) 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) + let policy = ArgPolicy (Set.singleton X0) (Set.singleton X0) Set.empty Set.empty st = seedArgs policy initTaintState assertEqual "X0 is secret" Secret (getTaint X0 st) @@ -803,7 +803,7 @@ taintConfigTests = testGroup "TaintConfig" [ , " ret" ] cfg = TaintConfig $ Map.singleton "_mul_wnaf" - (ArgPolicy (Set.singleton X0) Set.empty) + (ArgPolicy (Set.singleton X0) Set.empty Set.empty Set.empty) case auditWithConfig cfg "test" src of Left e -> assertFailure $ "parse failed: " ++ show e Right ar -> do @@ -821,7 +821,7 @@ taintConfigTests = testGroup "TaintConfig" [ , " ret" ] cfg = TaintConfig $ Map.singleton "_foo" - (ArgPolicy Set.empty (Set.singleton X0)) + (ArgPolicy Set.empty (Set.singleton X0) Set.empty Set.empty) case auditWithConfig cfg "test" src of Left e -> assertFailure $ "parse failed: " ++ show e Right ar -> assertEqual "no violations" 0 (length (arViolations ar)) @@ -833,9 +833,85 @@ taintConfigTests = testGroup "TaintConfig" [ , " ret" ] cfg = TaintConfig $ Map.singleton "_mul_wnaf" - (ArgPolicy (Set.singleton X0) Set.empty) + (ArgPolicy (Set.singleton X0) Set.empty Set.empty Set.empty) case auditInterProcWithConfig cfg "test" src of Left e -> assertFailure $ "parse failed: " ++ show e Right ar -> do assertEqual "one violation" 1 (length (arViolations ar)) + + -- STG stack slot seeding tests + , testCase "parse stg_secret/stg_public in config" $ do + let json = B8.pack $ unlines + [ "{" + , " \"_foo\": {" + , " \"secret\": [\"X0\"]," + , " \"stg_secret\": [8, 152]," + , " \"stg_public\": [24]" + , " }" + , "}" + ] + case eitherDecodeStrict' json :: Either String TaintConfig of + Left e -> assertFailure $ "parse failed: " ++ e + Right cfg -> do + let policy = Map.lookup "_foo" (tcPolicies cfg) + case policy of + Nothing -> assertFailure "missing policy for '_foo'" + Just p -> do + assertEqual "stg_secret" (Set.fromList [8, 152]) (apStgSecret p) + assertEqual "stg_public" (Set.singleton 24) (apStgPublic p) + + , testCase "stg_secret seeds STG stack slot as secret" $ do + -- Load from seeded secret STG stack slot should yield secret + let src = T.unlines + [ "_foo:" + , " ldr x8, [x20, #8]" -- Load from secret STG slot + , " ldr x9, [x21, x8]" -- Use as index -> violation + , " ret" + ] + cfg = TaintConfig $ Map.singleton "_foo" + (ArgPolicy Set.empty Set.empty (Set.singleton 8) Set.empty) + 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] -> case vReason v of + SecretIndex X8 -> pure () + other -> assertFailure $ "wrong reason: " ++ show other + _ -> assertFailure "expected one violation" + + , testCase "stg_public seeds STG stack slot as public" $ do + -- Load from seeded public STG stack slot should yield public + let src = T.unlines + [ "_foo:" + , " ldr x8, [x20, #16]" -- Load from public STG slot + , " ldr x9, [x21, x8]" -- Use as index -> should be safe + , " ret" + ] + cfg = TaintConfig $ Map.singleton "_foo" + (ArgPolicy Set.empty Set.empty Set.empty (Set.singleton 16)) + case auditWithConfig cfg "test" src of + Left e -> assertFailure $ "parse failed: " ++ show e + Right ar -> assertEqual "no violations" 0 (length (arViolations ar)) + + , testCase "stg_secret takes precedence over stg_public" $ do + -- If same offset in both lists, secret wins + let src = T.unlines + [ "_foo:" + , " ldr x8, [x20, #8]" -- Load from slot in both lists + , " ldr x9, [x21, x8]" -- Use as index -> violation (secret wins) + , " ret" + ] + cfg = TaintConfig $ Map.singleton "_foo" + (ArgPolicy Set.empty Set.empty + (Set.singleton 8) (Set.singleton 8)) + 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] -> case vReason v of + SecretIndex X8 -> pure () + other -> assertFailure $ "wrong reason: " ++ show other + _ -> assertFailure "expected one violation" ]