Types.hs (16938B)
1 {-# OPTIONS_HADDOCK prune #-} 2 {-# LANGUAGE DeriveAnyClass #-} 3 {-# LANGUAGE DeriveGeneric #-} 4 {-# LANGUAGE OverloadedStrings #-} 5 6 -- | 7 -- Module: Audit.AArch64.Types 8 -- Copyright: (c) 2025 Jared Tobin 9 -- License: MIT 10 -- Maintainer: jared@ppad.tech 11 -- 12 -- Core types for AArch64 assembly analysis. 13 14 module Audit.AArch64.Types ( 15 -- * Registers 16 Reg(..) 17 , regName 18 , regFromText 19 20 -- * Operands and addressing 21 , Shift(..) 22 , Extend(..) 23 , Operand(..) 24 , AddrMode(..) 25 26 -- * Instructions 27 , Instr(..) 28 , Line(..) 29 30 -- * Taint lattice 31 , Taint(..) 32 , joinTaint 33 34 -- * Provenance 35 , Provenance(..) 36 , joinProvenance 37 38 -- * Register kind 39 , RegKind(..) 40 , joinKind 41 42 -- * Analysis results 43 , Violation(..) 44 , ViolationReason(..) 45 46 -- * Non-constant-time findings 47 , NctReason(..) 48 , NctFinding(..) 49 , LineMap 50 51 -- * Taint configuration 52 , TaintConfig(..) 53 , defaultTaintConfig 54 , ArgPolicy(..) 55 , emptyArgPolicy 56 ) where 57 58 import Control.DeepSeq (NFData) 59 import Data.Aeson (ToJSON(..), FromJSON(..), (.=), (.:?), object, withObject) 60 import Data.IntMap.Strict (IntMap) 61 import Data.Map.Strict (Map) 62 import qualified Data.Map.Strict as Map 63 import Data.Set (Set) 64 import qualified Data.Set as Set 65 import Data.Text (Text) 66 import qualified Data.Text as T 67 import GHC.Generics (Generic) 68 69 -- | AArch64 registers (64-bit, 32-bit views, and SIMD). 70 data Reg 71 -- 64-bit general purpose 72 = X0 | X1 | X2 | X3 | X4 | X5 | X6 | X7 73 | X8 | X9 | X10 | X11 | X12 | X13 | X14 | X15 74 | X16 | X17 | X18 | X19 | X20 | X21 | X22 | X23 75 | X24 | X25 | X26 | X27 | X28 | X29 | X30 76 -- 32-bit views 77 | W0 | W1 | W2 | W3 | W4 | W5 | W6 | W7 78 | W8 | W9 | W10 | W11 | W12 | W13 | W14 | W15 79 | W16 | W17 | W18 | W19 | W20 | W21 | W22 | W23 80 | W24 | W25 | W26 | W27 | W28 | W29 | W30 81 -- Special 82 | SP -- ^ Stack pointer 83 | XZR -- ^ Zero register (64-bit) 84 | WZR -- ^ Zero register (32-bit) 85 -- SIMD/FP (64-bit double) 86 | D0 | D1 | D2 | D3 | D4 | D5 | D6 | D7 87 | D8 | D9 | D10 | D11 | D12 | D13 | D14 | D15 88 | D16 | D17 | D18 | D19 | D20 | D21 | D22 | D23 89 | D24 | D25 | D26 | D27 | D28 | D29 | D30 | D31 90 -- SIMD/FP (32-bit single) 91 | S0 | S1 | S2 | S3 | S4 | S5 | S6 | S7 92 | S8 | S9 | S10 | S11 | S12 | S13 | S14 | S15 93 | S16 | S17 | S18 | S19 | S20 | S21 | S22 | S23 94 | S24 | S25 | S26 | S27 | S28 | S29 | S30 | S31 95 -- SIMD/FP (128-bit quad) 96 | Q0 | Q1 | Q2 | Q3 | Q4 | Q5 | Q6 | Q7 97 | Q8 | Q9 | Q10 | Q11 | Q12 | Q13 | Q14 | Q15 98 | Q16 | Q17 | Q18 | Q19 | Q20 | Q21 | Q22 | Q23 99 | Q24 | Q25 | Q26 | Q27 | Q28 | Q29 | Q30 | Q31 100 deriving (Eq, Ord, Show, Generic, NFData) 101 102 instance ToJSON Reg where 103 toJSON = toJSON . regName 104 105 -- | Canonical lowercase register name. 106 regName :: Reg -> Text 107 regName r = T.toLower (T.pack (show r)) 108 109 -- | Parse a register from text (case-insensitive). 110 regFromText :: Text -> Maybe Reg 111 regFromText t = Map.lookup (T.toUpper t) regMap 112 where 113 regMap :: Map Text Reg 114 regMap = Map.fromList 115 [ ("X0", X0), ("X1", X1), ("X2", X2), ("X3", X3) 116 , ("X4", X4), ("X5", X5), ("X6", X6), ("X7", X7) 117 , ("X8", X8), ("X9", X9), ("X10", X10), ("X11", X11) 118 , ("X12", X12), ("X13", X13), ("X14", X14), ("X15", X15) 119 , ("X16", X16), ("X17", X17), ("X18", X18), ("X19", X19) 120 , ("X20", X20), ("X21", X21), ("X22", X22), ("X23", X23) 121 , ("X24", X24), ("X25", X25), ("X26", X26), ("X27", X27) 122 , ("X28", X28), ("X29", X29), ("X30", X30) 123 , ("W0", W0), ("W1", W1), ("W2", W2), ("W3", W3) 124 , ("W4", W4), ("W5", W5), ("W6", W6), ("W7", W7) 125 , ("W8", W8), ("W9", W9), ("W10", W10), ("W11", W11) 126 , ("W12", W12), ("W13", W13), ("W14", W14), ("W15", W15) 127 , ("W16", W16), ("W17", W17), ("W18", W18), ("W19", W19) 128 , ("W20", W20), ("W21", W21), ("W22", W22), ("W23", W23) 129 , ("W24", W24), ("W25", W25), ("W26", W26), ("W27", W27) 130 , ("W28", W28), ("W29", W29), ("W30", W30) 131 , ("SP", SP), ("XZR", XZR), ("WZR", WZR) 132 , ("D0", D0), ("D1", D1), ("D2", D2), ("D3", D3) 133 , ("D4", D4), ("D5", D5), ("D6", D6), ("D7", D7) 134 , ("D8", D8), ("D9", D9), ("D10", D10), ("D11", D11) 135 , ("D12", D12), ("D13", D13), ("D14", D14), ("D15", D15) 136 , ("D16", D16), ("D17", D17), ("D18", D18), ("D19", D19) 137 , ("D20", D20), ("D21", D21), ("D22", D22), ("D23", D23) 138 , ("D24", D24), ("D25", D25), ("D26", D26), ("D27", D27) 139 , ("D28", D28), ("D29", D29), ("D30", D30), ("D31", D31) 140 , ("S0", S0), ("S1", S1), ("S2", S2), ("S3", S3) 141 , ("S4", S4), ("S5", S5), ("S6", S6), ("S7", S7) 142 , ("S8", S8), ("S9", S9), ("S10", S10), ("S11", S11) 143 , ("S12", S12), ("S13", S13), ("S14", S14), ("S15", S15) 144 , ("S16", S16), ("S17", S17), ("S18", S18), ("S19", S19) 145 , ("S20", S20), ("S21", S21), ("S22", S22), ("S23", S23) 146 , ("S24", S24), ("S25", S25), ("S26", S26), ("S27", S27) 147 , ("S28", S28), ("S29", S29), ("S30", S30), ("S31", S31) 148 , ("Q0", Q0), ("Q1", Q1), ("Q2", Q2), ("Q3", Q3) 149 , ("Q4", Q4), ("Q5", Q5), ("Q6", Q6), ("Q7", Q7) 150 , ("Q8", Q8), ("Q9", Q9), ("Q10", Q10), ("Q11", Q11) 151 , ("Q12", Q12), ("Q13", Q13), ("Q14", Q14), ("Q15", Q15) 152 , ("Q16", Q16), ("Q17", Q17), ("Q18", Q18), ("Q19", Q19) 153 , ("Q20", Q20), ("Q21", Q21), ("Q22", Q22), ("Q23", Q23) 154 , ("Q24", Q24), ("Q25", Q25), ("Q26", Q26), ("Q27", Q27) 155 , ("Q28", Q28), ("Q29", Q29), ("Q30", Q30), ("Q31", Q31) 156 ] 157 158 -- | Shift operations for indexed addressing. 159 data Shift 160 = LSL !Int -- ^ Logical shift left 161 | LSR !Int -- ^ Logical shift right 162 | ASR !Int -- ^ Arithmetic shift right 163 deriving (Eq, Show, Generic, NFData) 164 165 instance ToJSON Shift 166 167 -- | Extend operations. 168 data Extend 169 = UXTW -- ^ Unsigned extend word 170 | SXTW -- ^ Signed extend word 171 | UXTX -- ^ Unsigned extend doubleword 172 | SXTX -- ^ Signed extend doubleword 173 deriving (Eq, Show, Generic, NFData) 174 175 instance ToJSON Extend 176 177 -- | Instruction operand. 178 data Operand 179 = OpReg !Reg -- ^ Register operand 180 | OpImm !Integer -- ^ Immediate value 181 | OpShiftedReg !Reg !Shift -- ^ Shifted register 182 | OpExtendedReg !Reg !Extend -- ^ Extended register 183 | OpLabel !Text -- ^ Label reference 184 | OpAddr !AddrMode -- ^ Memory address 185 deriving (Eq, Show, Generic, NFData) 186 187 instance ToJSON Operand 188 189 -- | Memory addressing modes. 190 data AddrMode 191 = BaseImm !Reg !Integer -- ^ [xN, #imm] or [xN] 192 | BaseReg !Reg !Reg -- ^ [xN, xM] 193 | BaseRegShift !Reg !Reg !Shift -- ^ [xN, xM, lsl #k] 194 | BaseRegExtend !Reg !Reg !Extend -- ^ [xN, xM, sxtw] 195 | BaseSymbol !Reg !Text -- ^ [xN, symbol@PAGEOFF] 196 | PreIndex !Reg !Integer -- ^ [xN, #imm]! 197 | PostIndex !Reg !Integer -- ^ [xN], #imm 198 | Literal !Text -- ^ =label or PC-relative 199 deriving (Eq, Show, Generic, NFData) 200 201 instance ToJSON AddrMode 202 203 -- | Parsed assembly instruction. 204 data Instr 205 -- Data movement 206 = Mov !Reg !Operand 207 | Movz !Reg !Integer !(Maybe Shift) 208 | Movk !Reg !Integer !(Maybe Shift) 209 | Movn !Reg !Integer !(Maybe Shift) 210 -- Arithmetic 211 | Add !Reg !Reg !Operand 212 | Sub !Reg !Reg !Operand 213 | Adds !Reg !Reg !Operand 214 | Subs !Reg !Reg !Operand 215 | Adc !Reg !Reg !Reg 216 | Adcs !Reg !Reg !Reg 217 | Sbc !Reg !Reg !Reg 218 | Neg !Reg !Operand 219 | Negs !Reg !Operand 220 | Mul !Reg !Reg !Reg 221 | Mneg !Reg !Reg !Reg 222 | Madd !Reg !Reg !Reg !Reg 223 | Msub !Reg !Reg !Reg !Reg 224 | Umulh !Reg !Reg !Reg 225 | Smulh !Reg !Reg !Reg 226 | Udiv !Reg !Reg !Reg 227 | Sdiv !Reg !Reg !Reg 228 -- Logical 229 | And !Reg !Reg !Operand 230 | Orr !Reg !Reg !Operand 231 | Eor !Reg !Reg !Operand 232 | Bic !Reg !Reg !Operand 233 | Mvn !Reg !Operand 234 | Tst !Reg !Operand 235 -- Shifts 236 | Lsl !Reg !Reg !Operand 237 | Lsr !Reg !Reg !Operand 238 | Asr !Reg !Reg !Operand 239 | Ror !Reg !Reg !Operand 240 -- Bit manipulation 241 | Ubfx !Reg !Reg !Int !Int 242 | Sbfx !Reg !Reg !Int !Int 243 | Bfi !Reg !Reg !Int !Int 244 | Extr !Reg !Reg !Reg !Int 245 -- Address generation 246 | Adr !Reg !Text 247 | Adrp !Reg !Text 248 -- Load/Store 249 | Ldr !Reg !AddrMode 250 | Ldrb !Reg !AddrMode 251 | Ldrh !Reg !AddrMode 252 | Ldrsb !Reg !AddrMode 253 | Ldrsh !Reg !AddrMode 254 | Ldrsw !Reg !AddrMode 255 | Ldur !Reg !AddrMode 256 | Str !Reg !AddrMode 257 | Strb !Reg !AddrMode 258 | Strh !Reg !AddrMode 259 | Stur !Reg !AddrMode 260 | Ldp !Reg !Reg !AddrMode 261 | Stp !Reg !Reg !AddrMode 262 -- Acquire/release loads and stores 263 | Ldar !Reg !AddrMode 264 | Ldarb !Reg !AddrMode 265 | Ldarh !Reg !AddrMode 266 | Stlr !Reg !AddrMode 267 | Stlrb !Reg !AddrMode 268 | Stlrh !Reg !AddrMode 269 -- Exclusive loads and stores 270 | Ldxr !Reg !AddrMode 271 | Ldxrb !Reg !AddrMode 272 | Ldxrh !Reg !AddrMode 273 | Stxr !Reg !Reg !AddrMode -- status, src, addr 274 | Stxrb !Reg !Reg !AddrMode 275 | Stxrh !Reg !Reg !AddrMode 276 -- Acquire-exclusive loads and release-exclusive stores 277 | Ldaxr !Reg !AddrMode 278 | Ldaxrb !Reg !AddrMode 279 | Ldaxrh !Reg !AddrMode 280 | Stlxr !Reg !Reg !AddrMode -- status, src, addr 281 | Stlxrb !Reg !Reg !AddrMode 282 | Stlxrh !Reg !Reg !AddrMode 283 -- Compare and select 284 | Cmp !Reg !Operand 285 | Cmn !Reg !Operand 286 | Csel !Reg !Reg !Reg !Text -- condition code 287 | Csinc !Reg !Reg !Reg !Text 288 | Csinv !Reg !Reg !Reg !Text 289 | Csneg !Reg !Reg !Reg !Text 290 | Cset !Reg !Text 291 | Cinc !Reg !Reg !Text 292 -- Branches 293 | B !Text 294 | BCond !Text !Text -- condition, target 295 | Bl !Text 296 | Blr !Reg 297 | Br !Reg 298 | Ret !(Maybe Reg) 299 | Cbz !Reg !Text 300 | Cbnz !Reg !Text 301 | Tbz !Reg !Int !Text 302 | Tbnz !Reg !Int !Text 303 -- System 304 | Nop 305 | Svc !Integer 306 -- Other (unparsed but recorded) 307 | Other !Text ![Text] 308 deriving (Eq, Show, Generic, NFData) 309 310 instance ToJSON Instr 311 312 -- | A line of assembly (with source location). 313 data Line = Line 314 { lineNum :: !Int 315 , lineLabel :: !(Maybe Text) 316 , lineInstr :: !(Maybe Instr) 317 } deriving (Eq, Show, Generic, NFData) 318 319 instance ToJSON Line 320 321 -- | Taint lattice for register publicness. 322 data Taint 323 = Public -- ^ Known to be public (derived from stack/heap pointers) 324 | Secret -- ^ Known or assumed to be secret 325 | Unknown -- ^ Not yet determined 326 deriving (Eq, Ord, Show, Generic, NFData) 327 328 instance ToJSON Taint 329 330 -- | Join operation for taint lattice (least upper bound). 331 -- For CT safety: Public only if both are Public. 332 -- Order: Public < Unknown < Secret 333 joinTaint :: Taint -> Taint -> Taint 334 joinTaint Public Public = Public 335 joinTaint Secret _ = Secret 336 joinTaint _ Secret = Secret 337 joinTaint _ _ = Unknown -- Public+Unknown or Unknown+Unknown 338 339 -- | Provenance: tracks whether a value derives from known-public sources. 340 -- Used to upgrade Unknown taint to Public when provenance can prove safety. 341 data Provenance 342 = ProvPublic -- ^ Derived from public root or constant 343 | ProvUnknown -- ^ Unknown origin (e.g., loaded from memory) 344 | ProvSecretData -- ^ Pointer to secret data (loads through it produce Secret) 345 deriving (Eq, Ord, Show, Generic, NFData) 346 347 instance ToJSON Provenance 348 349 -- | Join provenance: ProvPublic only if both are ProvPublic. 350 -- ProvSecretData dominates ProvPublic (conservative: might point to secrets). 351 -- ProvUnknown dominates everything (can't prove anything). 352 joinProvenance :: Provenance -> Provenance -> Provenance 353 joinProvenance ProvPublic ProvPublic = ProvPublic 354 joinProvenance ProvSecretData ProvSecretData = ProvSecretData 355 joinProvenance ProvSecretData ProvPublic = ProvSecretData 356 joinProvenance ProvPublic ProvSecretData = ProvSecretData 357 joinProvenance _ _ = ProvUnknown 358 359 -- | Register kind: distinguishes pointers from scalars. 360 -- Used to restrict provenance upgrades to pointer-kind registers only. 361 data RegKind 362 = KindPtr -- ^ Known to be a pointer (from adr/adrp or pointer arithmetic) 363 | KindScalar -- ^ Known to be a scalar (from loads or arithmetic) 364 | KindUnknown -- ^ Unknown kind 365 deriving (Eq, Ord, Show, Generic, NFData) 366 367 instance ToJSON RegKind 368 369 -- | Join register kinds: Ptr only if both are Ptr. 370 joinKind :: RegKind -> RegKind -> RegKind 371 joinKind KindPtr KindPtr = KindPtr 372 joinKind KindScalar _ = KindScalar 373 joinKind _ KindScalar = KindScalar 374 joinKind _ _ = KindUnknown 375 376 -- | Reason for a violation. 377 data ViolationReason 378 = SecretBase !Reg -- ^ Base register is secret 379 | SecretIndex !Reg -- ^ Index register is secret 380 | UnknownBase !Reg -- ^ Base register taint unknown 381 | UnknownIndex !Reg -- ^ Index register taint unknown 382 | NonConstOffset -- ^ Non-constant offset without masking 383 deriving (Eq, Show, Generic, NFData) 384 385 instance ToJSON ViolationReason where 386 toJSON (SecretBase r) = 387 object ["type" .= ("secret_base" :: Text), "register" .= r] 388 toJSON (SecretIndex r) = 389 object ["type" .= ("secret_index" :: Text), "register" .= r] 390 toJSON (UnknownBase r) = 391 object ["type" .= ("unknown_base" :: Text), "register" .= r] 392 toJSON (UnknownIndex r) = 393 object ["type" .= ("unknown_index" :: Text), "register" .= r] 394 toJSON NonConstOffset = 395 object ["type" .= ("non_const_offset" :: Text)] 396 397 -- | A memory access violation. 398 data Violation = Violation 399 { vSymbol :: !Text 400 , vLine :: !Int 401 , vInstr :: !Instr 402 , vReason :: !ViolationReason 403 } deriving (Eq, Show, Generic, NFData) 404 405 instance ToJSON Violation where 406 toJSON v = object 407 [ "symbol" .= vSymbol v 408 , "line" .= vLine v 409 , "instr" .= show (vInstr v) 410 , "reason" .= vReason v 411 ] 412 413 -- | Reason for flagging an instruction as non-constant-time. 414 data NctReason 415 = CondBranch -- ^ Conditional branch 416 | IndirectBranch -- ^ Indirect branch (br, blr) 417 | Div -- ^ Division (udiv, sdiv) 418 | RegIndexAddr -- ^ Register-indexed memory access 419 deriving (Eq, Ord, Show, Generic, NFData) 420 421 -- | A non-constant-time finding. 422 data NctFinding = NctFinding 423 { nctLine :: !Int -- ^ Source line number 424 , nctInstr :: !Instr -- ^ The flagged instruction 425 , nctReason :: !NctReason -- ^ Why it was flagged 426 } deriving (Eq, Show, Generic, NFData) 427 428 -- | Line number to Line map for efficient lookup. 429 type LineMap = IntMap Line 430 431 -- | Per-function argument taint policy. 432 -- Specifies which registers and STG stack slots should be seeded. 433 data ArgPolicy = ArgPolicy 434 { apSecret :: !(Set Reg) 435 -- ^ Registers to mark as Secret (scalar values) 436 , apPublic :: !(Set Reg) 437 -- ^ Registers to mark as Public 438 , apSecretPointee :: !(Set Reg) 439 -- ^ Registers that are pointers to secret data. 440 -- The pointer itself is public, but loads through it produce Secret values. 441 , apStgSecret :: !(Set Int) 442 -- ^ STG stack offsets (x20-relative) to mark Secret 443 , apStgPublic :: !(Set Int) 444 -- ^ STG stack offsets (x20-relative) to mark Public 445 } deriving (Eq, Show) 446 447 -- | Empty argument policy (no overrides). 448 emptyArgPolicy :: ArgPolicy 449 emptyArgPolicy = ArgPolicy Set.empty Set.empty Set.empty Set.empty Set.empty 450 451 instance FromJSON ArgPolicy where 452 parseJSON = withObject "ArgPolicy" $ \o -> do 453 secretTexts <- o .:? "secret" 454 publicTexts <- o .:? "public" 455 secretPointeeTexts <- o .:? "secret_pointee" 456 stgSecretInts <- o .:? "stg_secret" 457 stgPublicInts <- o .:? "stg_public" 458 let parseRegs :: Maybe [Text] -> Either Text (Set Reg) 459 parseRegs Nothing = Right Set.empty 460 parseRegs (Just ts) = 461 let parsed = map (\t -> (t, regFromText t)) ts 462 bad = [t | (t, Nothing) <- parsed] 463 in case bad of 464 [] -> Right $ Set.fromList [r | (_, Just r) <- parsed] 465 (b:_) -> Left $ "invalid register: " <> b 466 parseInts :: Maybe [Int] -> Set Int 467 parseInts Nothing = Set.empty 468 parseInts (Just is) = Set.fromList is 469 case (parseRegs secretTexts, parseRegs publicTexts, parseRegs secretPointeeTexts) of 470 (Left e, _, _) -> fail (T.unpack e) 471 (_, Left e, _) -> fail (T.unpack e) 472 (_, _, Left e) -> fail (T.unpack e) 473 (Right s, Right p, Right sp) -> pure $ ArgPolicy s p sp 474 (parseInts stgSecretInts) (parseInts stgPublicInts) 475 476 -- | Taint configuration: maps function symbols to argument policies. 477 -- Also controls global analysis assumptions. 478 data TaintConfig = TaintConfig 479 { tcPolicies :: !(Map Text ArgPolicy) 480 -- ^ Per-function argument taint policies 481 , tcAssumeStgPublic :: !Bool 482 -- ^ Assume untracked STG stack slots are public pointers (default: True). 483 -- GHC's STG stack holds closure pointers and return addresses, which are 484 -- inherently public. Set to False for paranoid mode. 485 } deriving (Eq, Show) 486 487 -- | Default taint config with no policies and STG-public assumption on. 488 defaultTaintConfig :: TaintConfig 489 defaultTaintConfig = TaintConfig 490 { tcPolicies = Map.empty 491 , tcAssumeStgPublic = True 492 } 493 494 instance FromJSON TaintConfig where 495 parseJSON v = do 496 policies <- parseJSON v 497 pure $ TaintConfig policies True