IMPL20.md (1271B)
1 # IMPL20: AArch64 Acquire/Release and Exclusive Memory Ops 2 3 ## Changes 4 5 1. Update instruction set (`lib/Audit/AArch64/Types.hs`): 6 - Add `Ldar/Ldarb/Ldarh`, `Stlr/Stlrb/Stlrh`. 7 - Add `Ldxr/Ldxrb/Ldxrh`, `Stxr/Stxrb/Stxrh`. 8 - Add `Ldaxr/Ldaxrb/Ldaxrh`, `Stlxr/Stlxrb/Stlxrh`. 9 - Model exclusive stores as `Stxr status src addr` (status is a reg). 10 11 2. Update parser (`lib/Audit/AArch64/Parser.hs`): 12 - Parse new mnemonics with the same address mode parser as `ldr/str`. 13 - For `stxr` family, parse status reg, src reg, addr. 14 15 3. Update taint transfer (`lib/Audit/AArch64/Taint.hs`): 16 - Treat new load variants like `Ldr/Ldrb/Ldrh`. 17 - Treat new store variants like `Str/Strb/Strh`. 18 - For `stxr`/`stlxr`, set status reg to Public/ProvPublic/KindScalar 19 after the store tracking. 20 21 4. Update memory access extraction (`lib/Audit/AArch64/Check.hs`): 22 - `getMemoryAccess` should include all new load/store variants. 23 24 5. Add tests (`test/Main.hs`): 25 - Minimal parsing tests for `ldar` and `stlr`. 26 - A taint test showing `ldar` from secret-derived address is flagged. 27 - A `stxr` test that confirms the status reg is Public and that the 28 store participates in stack tracking. 29 30 ## Notes 31 32 - Keep lines under 80 chars. 33 - Avoid new dependencies.