commit e48ce759831e9ac6983f51def00e72b451739be0
parent 8153ab942cbfd3b0df7cfb4851f91d5ac4ab8a22
Author: Jared Tobin <jared@jtobin.io>
Date: Wed, 11 Feb 2026 22:47:22 +0400
feat: add acquire/release and exclusive memory ops (IMPL20)
Extend parser, instruction set, and checker to recognize AArch64
load/store variants with acquire/release or exclusive semantics.
New instructions:
- Acquire loads: ldar, ldarb, ldarh
- Release stores: stlr, stlrb, stlrh
- Exclusive loads: ldxr, ldxrb, ldxrh
- Exclusive stores: stxr, stxrb, stxrh (status, src, addr)
- Acquire-exclusive: ldaxr, ldaxrb, ldaxrh
- Release-exclusive: stlxr, stlxrb, stlxrh (status, src, addr)
Semantics:
- Load variants treated same as ldr/ldrb/ldrh
- Store variants treated same as str/strb/strh
- Exclusive store status register set to Public/ProvPublic/KindScalar
Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com>
Diffstat:
7 files changed, 292 insertions(+), 1 deletion(-)
diff --git a/lib/Audit/AArch64/Check.hs b/lib/Audit/AArch64/Check.hs
@@ -118,7 +118,28 @@ getMemoryAccess instr = case instr of
Stur _ addr -> Just addr
Ldp _ _ addr -> Just addr
Stp _ _ addr -> Just addr
- _ -> Nothing
+ -- Acquire/release loads and stores
+ Ldar _ addr -> Just addr
+ Ldarb _ addr -> Just addr
+ Ldarh _ addr -> Just addr
+ Stlr _ addr -> Just addr
+ Stlrb _ addr -> Just addr
+ Stlrh _ addr -> Just addr
+ -- Exclusive loads and stores
+ Ldxr _ addr -> Just addr
+ Ldxrb _ addr -> Just addr
+ Ldxrh _ addr -> Just addr
+ Stxr _ _ addr -> Just addr
+ Stxrb _ _ addr -> Just addr
+ Stxrh _ _ addr -> Just addr
+ -- Acquire-exclusive and release-exclusive
+ Ldaxr _ addr -> Just addr
+ Ldaxrb _ addr -> Just addr
+ Ldaxrh _ addr -> Just addr
+ Stlxr _ _ addr -> Just addr
+ Stlxrb _ _ addr -> Just addr
+ Stlxrh _ _ addr -> Just addr
+ _ -> Nothing
-- | Check an addressing mode for violations.
checkAddrMode :: Text -> Int -> Instr -> AddrMode -> TaintState -> [Violation]
diff --git a/lib/Audit/AArch64/Parser.hs b/lib/Audit/AArch64/Parser.hs
@@ -213,6 +213,30 @@ parseByMnemonic m = case m of
"ldp" -> Ldp <$> pReg <*> (pComma *> pReg) <*> (pComma *> pAddrMode)
"stp" -> Stp <$> pReg <*> (pComma *> pReg) <*> (pComma *> pAddrMode)
+ -- Acquire/release loads and stores
+ "ldar" -> Ldar <$> pReg <*> (pComma *> pAddrMode)
+ "ldarb" -> Ldarb <$> pReg <*> (pComma *> pAddrMode)
+ "ldarh" -> Ldarh <$> pReg <*> (pComma *> pAddrMode)
+ "stlr" -> Stlr <$> pReg <*> (pComma *> pAddrMode)
+ "stlrb" -> Stlrb <$> pReg <*> (pComma *> pAddrMode)
+ "stlrh" -> Stlrh <$> pReg <*> (pComma *> pAddrMode)
+
+ -- Exclusive loads and stores
+ "ldxr" -> Ldxr <$> pReg <*> (pComma *> pAddrMode)
+ "ldxrb" -> Ldxrb <$> pReg <*> (pComma *> pAddrMode)
+ "ldxrh" -> Ldxrh <$> pReg <*> (pComma *> pAddrMode)
+ "stxr" -> Stxr <$> pReg <*> (pComma *> pReg) <*> (pComma *> pAddrMode)
+ "stxrb" -> Stxrb <$> pReg <*> (pComma *> pReg) <*> (pComma *> pAddrMode)
+ "stxrh" -> Stxrh <$> pReg <*> (pComma *> pReg) <*> (pComma *> pAddrMode)
+
+ -- Acquire-exclusive loads and release-exclusive stores
+ "ldaxr" -> Ldaxr <$> pReg <*> (pComma *> pAddrMode)
+ "ldaxrb" -> Ldaxrb <$> pReg <*> (pComma *> pAddrMode)
+ "ldaxrh" -> Ldaxrh <$> pReg <*> (pComma *> pAddrMode)
+ "stlxr" -> Stlxr <$> pReg <*> (pComma *> pReg) <*> (pComma *> pAddrMode)
+ "stlxrb" -> Stlxrb <$> pReg <*> (pComma *> pReg) <*> (pComma *> pAddrMode)
+ "stlxrh" -> Stlxrh <$> pReg <*> (pComma *> pReg) <*> (pComma *> pAddrMode)
+
-- Compare and select
"cmp" -> Cmp <$> pReg <*> (pComma *> pOperand)
"cmn" -> Cmn <$> pReg <*> (pComma *> pOperand)
diff --git a/lib/Audit/AArch64/Taint.hs b/lib/Audit/AArch64/Taint.hs
@@ -388,6 +388,48 @@ transfer instr st = case instr of
Stur src addr -> storeToStack src addr st
Stp src1 src2 addr -> storePairToStack src1 src2 addr st
+ -- Acquire/release loads (same as regular loads)
+ Ldar dst addr -> loadFromStack dst addr st
+ Ldarb dst addr -> loadFromStack dst addr st
+ Ldarh dst addr -> loadFromStack dst addr st
+
+ -- Release stores (same as regular stores)
+ Stlr src addr -> storeToStack src addr st
+ Stlrb src addr -> storeToStack src addr st
+ Stlrh src addr -> storeToStack src addr st
+
+ -- Exclusive loads (same as regular loads)
+ Ldxr dst addr -> loadFromStack dst addr st
+ Ldxrb dst addr -> loadFromStack dst addr st
+ Ldxrh dst addr -> loadFromStack dst addr st
+
+ -- Exclusive stores: status reg is Public scalar, src participates in store
+ Stxr status src addr ->
+ let st' = storeToStack src addr st
+ in setTaintProvKind status Public ProvPublic KindScalar st'
+ Stxrb status src addr ->
+ let st' = storeToStack src addr st
+ in setTaintProvKind status Public ProvPublic KindScalar st'
+ Stxrh status src addr ->
+ let st' = storeToStack src addr st
+ in setTaintProvKind status Public ProvPublic KindScalar st'
+
+ -- Acquire-exclusive loads (same as regular loads)
+ Ldaxr dst addr -> loadFromStack dst addr st
+ Ldaxrb dst addr -> loadFromStack dst addr st
+ Ldaxrh dst addr -> loadFromStack dst addr st
+
+ -- Release-exclusive stores: status reg is Public scalar
+ Stlxr status src addr ->
+ let st' = storeToStack src addr st
+ in setTaintProvKind status Public ProvPublic KindScalar st'
+ Stlxrb status src addr ->
+ let st' = storeToStack src addr st
+ in setTaintProvKind status Public ProvPublic KindScalar st'
+ Stlxrh status src addr ->
+ let st' = storeToStack src addr st
+ in setTaintProvKind status Public ProvPublic KindScalar st'
+
-- Conditionals: result is scalar (conservative)
Cmp _ _ -> st
Cmn _ _ -> st
diff --git a/lib/Audit/AArch64/Types.hs b/lib/Audit/AArch64/Types.hs
@@ -252,6 +252,27 @@ data Instr
| Stur !Reg !AddrMode
| Ldp !Reg !Reg !AddrMode
| Stp !Reg !Reg !AddrMode
+ -- Acquire/release loads and stores
+ | Ldar !Reg !AddrMode
+ | Ldarb !Reg !AddrMode
+ | Ldarh !Reg !AddrMode
+ | Stlr !Reg !AddrMode
+ | Stlrb !Reg !AddrMode
+ | Stlrh !Reg !AddrMode
+ -- Exclusive loads and stores
+ | Ldxr !Reg !AddrMode
+ | Ldxrb !Reg !AddrMode
+ | Ldxrh !Reg !AddrMode
+ | Stxr !Reg !Reg !AddrMode -- status, src, addr
+ | Stxrb !Reg !Reg !AddrMode
+ | Stxrh !Reg !Reg !AddrMode
+ -- Acquire-exclusive loads and release-exclusive stores
+ | Ldaxr !Reg !AddrMode
+ | Ldaxrb !Reg !AddrMode
+ | Ldaxrh !Reg !AddrMode
+ | Stlxr !Reg !Reg !AddrMode -- status, src, addr
+ | Stlxrb !Reg !Reg !AddrMode
+ | Stlxrh !Reg !Reg !AddrMode
-- Compare and select
| Cmp !Reg !Operand
| Cmn !Reg !Operand
diff --git a/plans/ARCH20.md b/plans/ARCH20.md
@@ -0,0 +1,52 @@
+# ARCH20: AArch64 Acquire/Release and Exclusive Memory Ops
+
+## Goal
+
+Extend the parser, instruction set, and checker to recognize AArch64
+load/store variants that carry acquire/release or exclusive semantics,
+so they are not silently ignored during auditing.
+
+## Context
+
+The current parser only handles basic `ldr/str` families. Instructions
+like `ldar`, `stlr`, `ldaxr`, `stlxr` appear in GHC output and represent
+memory accesses that should be taint-checked. Missing them results in
+false negatives.
+
+## Approach
+
+Treat these as normal memory accesses for the purposes of taint
+propagation and violation checks:
+
+- Acquire loads: `ldar`, `ldarb`, `ldarh`
+- Release stores: `stlr`, `stlrb`, `stlrh`
+- Exclusive loads: `ldxr`, `ldxrb`, `ldxrh`
+- Exclusive stores: `stxr`, `stxrb`, `stxrh`
+- Acquire-exclusive loads: `ldaxr`, `ldaxrb`, `ldaxrh`
+- Release-exclusive stores: `stlxr`, `stlxrb`, `stlxrh`
+
+Semantics:
+
+- Load variants update taint of destination register using the same
+ rules as `ldr` / `ldrb` / `ldrh`.
+- Store variants update stack/heap tracking using the same rules as
+ `str` / `strb` / `strh`.
+- The exclusive result register (e.g., `stxr wX, wY, [xZ]`) does not
+ carry taint from the store; it is a scalar status. Treat it as
+ Public/ProvPublic/KindScalar.
+
+## Scope
+
+- Update `Instr` constructors, parser, and checker.
+- Update taint transfer for new instructions.
+- Update memory access extraction for `checkLineStrict`.
+
+## Risks
+
+- Slightly increased parser/transfer surface area.
+- If we miss an opcode in the family, it will remain untracked.
+
+## Out of Scope
+
+- Atomic RMW instructions (`ldadd`, `swp`, `cas`, etc.).
+ Consider in a later iteration if needed.
diff --git a/plans/IMPL20.md b/plans/IMPL20.md
@@ -0,0 +1,33 @@
+# IMPL20: AArch64 Acquire/Release and Exclusive Memory Ops
+
+## Changes
+
+1. Update instruction set (`lib/Audit/AArch64/Types.hs`):
+ - Add `Ldar/Ldarb/Ldarh`, `Stlr/Stlrb/Stlrh`.
+ - Add `Ldxr/Ldxrb/Ldxrh`, `Stxr/Stxrb/Stxrh`.
+ - Add `Ldaxr/Ldaxrb/Ldaxrh`, `Stlxr/Stlxrb/Stlxrh`.
+ - Model exclusive stores as `Stxr status src addr` (status is a reg).
+
+2. Update parser (`lib/Audit/AArch64/Parser.hs`):
+ - Parse new mnemonics with the same address mode parser as `ldr/str`.
+ - For `stxr` family, parse status reg, src reg, addr.
+
+3. Update taint transfer (`lib/Audit/AArch64/Taint.hs`):
+ - Treat new load variants like `Ldr/Ldrb/Ldrh`.
+ - Treat new store variants like `Str/Strb/Strh`.
+ - For `stxr`/`stlxr`, set status reg to Public/ProvPublic/KindScalar
+ after the store tracking.
+
+4. Update memory access extraction (`lib/Audit/AArch64/Check.hs`):
+ - `getMemoryAccess` should include all new load/store variants.
+
+5. Add tests (`test/Main.hs`):
+ - Minimal parsing tests for `ldar` and `stlr`.
+ - A taint test showing `ldar` from secret-derived address is flagged.
+ - A `stxr` test that confirms the status reg is Public and that the
+ store participates in stack tracking.
+
+## Notes
+
+- Keep lines under 80 chars.
+- Avoid new dependencies.
diff --git a/test/Main.hs b/test/Main.hs
@@ -141,6 +141,47 @@ parserTests = testGroup "Parser" [
Right lns -> case safeHead lns of
Line _ Nothing (Just (Mov X0 (OpReg X1))) -> pure ()
other -> assertFailure $ "unexpected: " ++ show other
+
+ -- Acquire/release and exclusive memory ops (IMPL20)
+ , testCase "parse ldar" $ do
+ let src = "ldar x0, [x1]\n"
+ case parseAsm src of
+ Left e -> assertFailure $ "parse failed: " ++ show e
+ Right lns -> case lineInstr (safeHead lns) of
+ Just (Ldar X0 (BaseImm X1 0)) -> pure ()
+ other -> assertFailure $ "unexpected: " ++ show other
+
+ , testCase "parse stlr" $ do
+ let src = "stlr x0, [x1]\n"
+ case parseAsm src of
+ Left e -> assertFailure $ "parse failed: " ++ show e
+ Right lns -> case lineInstr (safeHead lns) of
+ Just (Stlr X0 (BaseImm X1 0)) -> pure ()
+ other -> assertFailure $ "unexpected: " ++ show other
+
+ , testCase "parse stxr" $ do
+ let src = "stxr w0, x1, [x2]\n"
+ case parseAsm src of
+ Left e -> assertFailure $ "parse failed: " ++ show e
+ Right lns -> case lineInstr (safeHead lns) of
+ Just (Stxr W0 X1 (BaseImm X2 0)) -> pure ()
+ other -> assertFailure $ "unexpected: " ++ show other
+
+ , testCase "parse ldaxr" $ do
+ let src = "ldaxr x0, [x1]\n"
+ case parseAsm src of
+ Left e -> assertFailure $ "parse failed: " ++ show e
+ Right lns -> case lineInstr (safeHead lns) of
+ Just (Ldaxr X0 (BaseImm X1 0)) -> pure ()
+ other -> assertFailure $ "unexpected: " ++ show other
+
+ , testCase "parse stlxr" $ do
+ let src = "stlxr w0, x1, [x2]\n"
+ case parseAsm src of
+ Left e -> assertFailure $ "parse failed: " ++ show e
+ Right lns -> case lineInstr (safeHead lns) of
+ Just (Stlxr W0 X1 (BaseImm X2 0)) -> pure ()
+ other -> assertFailure $ "unexpected: " ++ show other
]
safeHead :: [a] -> a
@@ -591,6 +632,63 @@ auditTests = testGroup "Audit" [
SecretIndex X9 -> pure ()
other -> assertFailure $ "wrong reason: " ++ show other
_ -> assertFailure "expected one violation"
+
+ -- Acquire/release and exclusive memory ops (IMPL20)
+ , testCase "bad: ldar from unknown base" $ do
+ -- ldar should be checked like ldr
+ let src = T.unlines
+ [ "_foo:"
+ , " ldar x8, [x0]" -- x0 is unknown -> violation
+ , " ret"
+ ]
+ case audit "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
+ UnknownBase X0 -> pure ()
+ other -> assertFailure $ "wrong reason: " ++ show other
+ _ -> assertFailure "expected one violation"
+
+ , testCase "good: stlr to stack preserves taint" $ do
+ -- stlr should track stack slots like str
+ let src = T.unlines
+ [ "_foo:"
+ , " adrp x8, _const@PAGE" -- x8 = public
+ , " stlr x8, [sp]" -- Store public to stack
+ , " ldr x9, [sp]" -- Reload -> public
+ , " ldr x10, [x9]" -- Use as base -> safe
+ , " ret"
+ ]
+ case audit "test" src of
+ Left e -> assertFailure $ "parse failed: " ++ show e
+ Right ar -> assertEqual "no violations" 0 (length (arViolations ar))
+
+ , testCase "good: stxr status register is public" $ do
+ -- stxr status register should be Public, allowing use as index
+ -- Note: w0 and x0 are separate in our model, so use w0 directly
+ let src = T.unlines
+ [ "_foo:"
+ , " stxr w0, x1, [x21]" -- w0 = status (public scalar)
+ , " ldr x8, [x20, w0]" -- Use w0 as index -> safe
+ , " ret"
+ ]
+ case audit "test" src of
+ Left e -> assertFailure $ "parse failed: " ++ show e
+ Right ar -> assertEqual "no violations" 0 (length (arViolations ar))
+
+ , testCase "good: stlxr status register is public" $ do
+ -- stlxr status register should be Public
+ let src = T.unlines
+ [ "_foo:"
+ , " stlxr w0, x1, [x21]" -- w0 = status (public scalar)
+ , " ldr x8, [x20, w0]" -- Use w0 as index -> safe
+ , " ret"
+ ]
+ case audit "test" src of
+ Left e -> assertFailure $ "parse failed: " ++ show e
+ Right ar -> assertEqual "no violations" 0 (length (arViolations ar))
]
-- Inter-procedural tests
