auditor

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

commit 6ae7b16a191faf0b0da81403533ecffef84c99be
parent 81df281f56455c489640898c6820a5674d93c81b
Author: Jared Tobin <jared@jtobin.io>
Date:   Fri, 13 Feb 2026 08:49:24 +0400

feat: add NCG tag check and arity check edge case detection (IMPL22)

Extend GHC runtime pattern detection to handle NCG-specific patterns:

- Tag check with `cmp reg, reg` where one register was set by `and #7`
  (NCG loads tag constant into register before comparing)

- Arity check with `ldr` (not just `ldur`) at negative offset from
  info pointer, with register-to-register comparison

- Add `samePhysicalReg` helper to match W/X register variants
  (NCG uses `ldr w10` but `cmp x10` - same physical register)

Both LLVM and NCG backends now show only 6 findings on Curve test
files, all in explicitly `_vartime` functions.

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

Diffstat:
Mlib/Audit/AArch64/NCT.hs | 63+++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++--
1 file changed, 61 insertions(+), 2 deletions(-)

diff --git a/lib/Audit/AArch64/NCT.hs b/lib/Audit/AArch64/NCT.hs @@ -206,10 +206,15 @@ isGhcRuntimeFinding lineMap f = case nctReason f of -- Pattern 1: tst <r>, #7 followed by branch (LLVM) -- Pattern 2: and <r>, <r2>, #7; cmp <r>, #N followed by branch (LLVM) -- Pattern 3: and <r>, <r2>, #7; cbnz/cbz <r> (NCG) + -- Pattern 4: and <r>, <r2>, #7; movz <r3>, #N; cmp <r>, <r3> (NCG) isTagCheck :: Bool isTagCheck = case prevInstr of Just (Tst _ (OpImm 7)) -> True Just (Cmp _ (OpImm _)) -> any isTagMask recentInstrs5 + Just (Cmp r1 (OpReg r2)) -> + -- NCG: cmp rA, rB where one was set by and #7 + any (isTagMaskFor r1) recentInstrs5 + || any (isTagMaskFor r2) recentInstrs5 _ -> case nctInstr f of -- NCG: cbnz/cbz on register set by and #7 Cbnz reg _ -> any (isTagMaskFor reg) recentInstrs5 @@ -227,17 +232,30 @@ isGhcRuntimeFinding lineMap f = case nctReason f of _ -> False -- Check if conditional branch is an arity/closure-type check - -- Pattern: ldur <r>, [<r2>, #-N] (info table access); cmp <r>, #M + -- Pattern 1: ldur <r>, [<r2>, #-N]; cmp <r>, #M (LLVM) + -- Pattern 2: ldr <r>, [<r2>, #-N]; cmp <r>, <r3> (NCG) -- Info tables are at negative offsets from info pointer isArityCheck :: Bool isArityCheck = case prevInstr of Just (Cmp _ (OpImm _)) -> any isInfoTableLoad recentInstrs5 - _ -> False + Just (Cmp r1 (OpReg r2)) -> + -- NCG: cmp rA, rB where one was loaded from info table + any (isInfoTableLoadFor r1) recentInstrs5 + || any (isInfoTableLoadFor r2) recentInstrs5 + _ -> False isInfoTableLoad :: Instr -> Bool isInfoTableLoad instr = case instr of -- Negative offset indicates info table field access Ldur _ (BaseImm _ off) -> off < 0 + Ldr _ (BaseImm _ off) -> off < 0 -- NCG uses ldr, not ldur + _ -> False + + isInfoTableLoadFor :: Reg -> Instr -> Bool + isInfoTableLoadFor reg instr = case instr of + -- Use samePhysicalReg since ldr w10 and cmp x10 are same register + Ldur r (BaseImm _ off) -> samePhysicalReg r reg && off < 0 + Ldr r (BaseImm _ off) -> samePhysicalReg r reg && off < 0 _ -> False -- Check if cbz/cbnz is a CAF check (recent: bl _newCAF or similar) @@ -372,3 +390,43 @@ filterGhcRuntime lns findings = Map.mapMaybe filterFindings findings filterFindings fs = let fs' = filter (not . isGhcRuntimeFinding lineMap) fs in if null fs' then Nothing else Just fs' + +-- | Check if two registers refer to the same physical register. +-- W and X variants of the same number are the same physical register. +samePhysicalReg :: Reg -> Reg -> Bool +samePhysicalReg r1 r2 = r1 == r2 || physNum r1 == physNum r2 + where + physNum :: Reg -> Maybe Int + physNum r = case r of + X0 -> Just 0; W0 -> Just 0 + X1 -> Just 1; W1 -> Just 1 + X2 -> Just 2; W2 -> Just 2 + X3 -> Just 3; W3 -> Just 3 + X4 -> Just 4; W4 -> Just 4 + X5 -> Just 5; W5 -> Just 5 + X6 -> Just 6; W6 -> Just 6 + X7 -> Just 7; W7 -> Just 7 + X8 -> Just 8; W8 -> Just 8 + X9 -> Just 9; W9 -> Just 9 + X10 -> Just 10; W10 -> Just 10 + X11 -> Just 11; W11 -> Just 11 + X12 -> Just 12; W12 -> Just 12 + X13 -> Just 13; W13 -> Just 13 + X14 -> Just 14; W14 -> Just 14 + X15 -> Just 15; W15 -> Just 15 + X16 -> Just 16; W16 -> Just 16 + X17 -> Just 17; W17 -> Just 17 + X18 -> Just 18; W18 -> Just 18 + X19 -> Just 19; W19 -> Just 19 + X20 -> Just 20; W20 -> Just 20 + X21 -> Just 21; W21 -> Just 21 + X22 -> Just 22; W22 -> Just 22 + X23 -> Just 23; W23 -> Just 23 + X24 -> Just 24; W24 -> Just 24 + X25 -> Just 25; W25 -> Just 25 + X26 -> Just 26; W26 -> Just 26 + X27 -> Just 27; W27 -> Just 27 + X28 -> Just 28; W28 -> Just 28 + X29 -> Just 29; W29 -> Just 29 + X30 -> Just 30; W30 -> Just 30 + _ -> Nothing -- SP, XZR, WZR, SIMD regs don't match +\ No newline at end of file