Check.hs (10400B)
1 {-# OPTIONS_HADDOCK prune #-} 2 {-# LANGUAGE BangPatterns #-} 3 {-# LANGUAGE DeriveAnyClass #-} 4 {-# LANGUAGE DeriveGeneric #-} 5 {-# LANGUAGE OverloadedStrings #-} 6 7 -- | 8 -- Module: Audit.AArch64.Check 9 -- Copyright: (c) 2025 Jared Tobin 10 -- License: MIT 11 -- Maintainer: jared@ppad.tech 12 -- 13 -- Memory access validation for constant-time properties. 14 -- 15 -- Checks that all memory accesses use public base registers 16 -- and constant (or properly masked) offsets. 17 18 module Audit.AArch64.Check ( 19 checkLine 20 , checkBlock 21 , checkCFG 22 , checkCFGInterProc 23 , checkCFGWithConfig 24 , checkCFGInterProcWithConfig 25 , AuditResult(..) 26 ) where 27 28 import Audit.AArch64.CFG 29 ( BasicBlock(..), CFG(..) 30 , cfgBlockCount, indexBlock, blockFunction 31 ) 32 import Audit.AArch64.Runtime 33 (RuntimeConfig(..), SecondaryStack(..)) 34 import Audit.AArch64.Taint 35 import Audit.AArch64.Types 36 ( Reg(..), Instr(..), Line(..), AddrMode(..) 37 , Taint(..), Provenance(..), RegKind(..) 38 , Violation(..), ViolationReason(..) 39 , TaintConfig(..) 40 ) 41 import Control.DeepSeq (NFData) 42 import qualified Data.IntMap.Strict as IM 43 import qualified Data.Map.Strict as Map 44 import Data.Maybe (fromMaybe) 45 import Data.Text (Text) 46 import GHC.Generics (Generic) 47 48 -- | Result of auditing assembly. 49 data AuditResult = AuditResult 50 { arViolations :: ![Violation] 51 , arLinesChecked :: !Int 52 , arMemoryAccesses :: !Int 53 } deriving (Eq, Show, Generic, NFData) 54 55 instance Semigroup AuditResult where 56 a <> b = AuditResult 57 { arViolations = 58 arViolations a ++ arViolations b 59 , arLinesChecked = 60 arLinesChecked a + arLinesChecked b 61 , arMemoryAccesses = 62 arMemoryAccesses a + arMemoryAccesses b 63 } 64 65 instance Monoid AuditResult where 66 mempty = AuditResult [] 0 0 67 68 -- | Check a single line for memory access violations. 69 checkLine :: Text -> TaintState -> Line -> AuditResult 70 checkLine sym st l = case lineInstr l of 71 Nothing -> AuditResult [] 1 0 72 Just instr -> case getMemoryAccess instr of 73 Nothing -> AuditResult [] 1 0 74 Just addr -> 75 let violations = 76 checkAddrMode sym (lineNum l) instr addr st 77 in AuditResult violations 1 1 78 79 -- | Check a basic block, threading taint state. 80 -- Uses strict counters and cons-accumulation for 81 -- violations. 82 checkBlock :: RuntimeConfig -> Text -> TaintState 83 -> [Line] -> (AuditResult, TaintState) 84 checkBlock rt sym st0 lns = go [] 0 0 st0 lns 85 where 86 go !vs !lc !ma st [] = 87 (AuditResult (reverse vs) lc ma, st) 88 go !vs !lc !ma st (l:ls) = 89 let (vs', ma') = checkLineStrict sym st l 90 st' = analyzeLine rt l st 91 in go (foldl' (flip (:)) vs vs') 92 (lc + 1) (ma + ma') st' ls 93 94 -- | Check a single line, returning violations and 95 -- memory access count. 96 checkLineStrict :: Text -> TaintState -> Line 97 -> ([Violation], Int) 98 checkLineStrict sym st l = case lineInstr l of 99 Nothing -> ([], 0) 100 Just instr -> case getMemoryAccess instr of 101 Nothing -> ([], 0) 102 Just addr -> 103 (checkAddrMode sym (lineNum l) instr addr st, 1) 104 105 -- | Check entire CFG with inter-block dataflow. 106 -- Runs fixpoint dataflow to propagate taint across blocks. 107 checkCFG :: RuntimeConfig -> Text -> CFG -> AuditResult 108 checkCFG rt sym cfg = 109 let inStates = runDataflow rt cfg 110 nBlocks = cfgBlockCount cfg 111 baseState = initTaintState rt 112 in mconcat 113 [ fst (checkBlock rt blockSym inState 114 (bbLines bb)) 115 | idx <- [0..nBlocks-1] 116 , let bb = indexBlock cfg idx 117 blockSym = maybe sym id (bbLabel bb) 118 inState = 119 IM.findWithDefault baseState 120 idx inStates 121 ] 122 123 -- | Extract memory address from a load/store instruction. 124 getMemoryAccess :: Instr -> Maybe AddrMode 125 getMemoryAccess instr = case instr of 126 Ldr _ addr -> Just addr 127 Ldrb _ addr -> Just addr 128 Ldrh _ addr -> Just addr 129 Ldrsb _ addr -> Just addr 130 Ldrsh _ addr -> Just addr 131 Ldrsw _ addr -> Just addr 132 Ldur _ addr -> Just addr 133 Str _ addr -> Just addr 134 Strb _ addr -> Just addr 135 Strh _ addr -> Just addr 136 Stur _ addr -> Just addr 137 Ldp _ _ addr -> Just addr 138 Stp _ _ addr -> Just addr 139 -- Acquire/release loads and stores 140 Ldar _ addr -> Just addr 141 Ldarb _ addr -> Just addr 142 Ldarh _ addr -> Just addr 143 Stlr _ addr -> Just addr 144 Stlrb _ addr -> Just addr 145 Stlrh _ addr -> Just addr 146 -- Exclusive loads and stores 147 Ldxr _ addr -> Just addr 148 Ldxrb _ addr -> Just addr 149 Ldxrh _ addr -> Just addr 150 Stxr _ _ addr -> Just addr 151 Stxrb _ _ addr -> Just addr 152 Stxrh _ _ addr -> Just addr 153 -- Acquire-exclusive and release-exclusive 154 Ldaxr _ addr -> Just addr 155 Ldaxrb _ addr -> Just addr 156 Ldaxrh _ addr -> Just addr 157 Stlxr _ _ addr -> Just addr 158 Stlxrb _ _ addr -> Just addr 159 Stlxrh _ _ addr -> Just addr 160 _ -> Nothing 161 162 -- | Check an addressing mode for violations. 163 checkAddrMode :: Text -> Int -> Instr -> AddrMode 164 -> TaintState -> [Violation] 165 checkAddrMode sym ln instr addr st = case addr of 166 BaseImm base _ -> 167 checkBase sym ln instr base st 168 169 BaseReg base idx -> 170 checkBase sym ln instr base st ++ 171 checkIndex sym ln instr idx st 172 173 BaseRegShift base idx _ -> 174 checkBase sym ln instr base st ++ 175 checkIndex sym ln instr idx st 176 177 BaseRegExtend base idx _ -> 178 checkBase sym ln instr base st ++ 179 checkIndex sym ln instr idx st 180 181 BaseSymbol base _ -> 182 -- Symbol offset is constant (compile-time), 183 -- only check base 184 checkBase sym ln instr base st 185 186 PreIndex base _ -> 187 checkBase sym ln instr base st 188 189 PostIndex base _ -> 190 checkBase sym ln instr base st 191 192 Literal _ -> 193 -- PC-relative literal: public 194 [] 195 196 -- | Check that base register is public. 197 -- If taint is Unknown, check provenance to see if we can 198 -- upgrade to Public. Provenance upgrade is only allowed 199 -- for pointer-kind registers to prevent laundering scalar 200 -- indices through provenance. 201 checkBase :: Text -> Int -> Instr -> Reg 202 -> TaintState -> [Violation] 203 checkBase sym ln instr base st = 204 case getTaint base st of 205 Public -> [] 206 Secret -> 207 [Violation sym ln instr (SecretBase base)] 208 Unknown -> 209 -- Only upgrade via provenance if register has 210 -- pointer kind 211 case (getProvenance base st, getKind base st) of 212 (ProvPublic, KindPtr) -> [] 213 _ -> 214 [Violation sym ln instr (UnknownBase base)] 215 216 -- | Check that index register is public. 217 -- If taint is Unknown, check provenance to see if we can 218 -- upgrade to Public. Index registers should never be 219 -- upgraded via provenance since they are typically scalars, 220 -- not pointers. 221 checkIndex :: Text -> Int -> Instr -> Reg 222 -> TaintState -> [Violation] 223 checkIndex sym ln instr idx st = 224 case getTaint idx st of 225 Public -> [] 226 Secret -> 227 [Violation sym ln instr (SecretIndex idx)] 228 Unknown -> 229 [Violation sym ln instr (UnknownIndex idx)] 230 -- No provenance upgrade for indices 231 232 -- | Check entire CFG with inter-procedural analysis. 233 -- Uses whole-file dataflow with summaries to propagate 234 -- taint across tail call boundaries. 235 checkCFGInterProc :: RuntimeConfig -> Text -> CFG 236 -> AuditResult 237 checkCFGInterProc rt sym cfg = 238 let summaries = runInterProc rt cfg 239 assumeStg = case rtSecondaryStack rt of 240 Nothing -> False 241 Just ss -> ssAssumePublic ss 242 emptyConfig = TaintConfig Map.empty assumeStg 243 inStates = 244 runDataflowWithConfigAndSummaries rt emptyConfig 245 summaries cfg 246 nBlocks = cfgBlockCount cfg 247 baseState = initTaintState rt 248 in mconcat 249 [ fst (checkBlockWithSummary rt blockSym 250 summaries inState (bbLines bb)) 251 | idx <- [0..nBlocks-1] 252 , let bb = indexBlock cfg idx 253 blockSym = 254 fromMaybe sym (blockFunction cfg idx) 255 inState = 256 IM.findWithDefault baseState 257 idx inStates 258 ] 259 260 -- | Check a block using summaries for calls. 261 -- Uses strict counters and cons-accumulation for 262 -- violations. 263 checkBlockWithSummary 264 :: RuntimeConfig -> Text -> Map.Map Text FuncSummary 265 -> TaintState -> [Line] 266 -> (AuditResult, TaintState) 267 checkBlockWithSummary rt sym summaries st0 lns = 268 go [] 0 0 st0 lns 269 where 270 go !vs !lc !ma st [] = 271 (AuditResult (reverse vs) lc ma, st) 272 go !vs !lc !ma st (l:ls) = 273 let (vs', ma') = checkLineStrict sym st l 274 st' = case lineInstr l of 275 Nothing -> st 276 Just instr -> case instr of 277 Bl target -> 278 case Map.lookup target summaries of 279 Just summ -> applySummary summ st 280 Nothing -> analyzeLine rt l st 281 _ -> analyzeLine rt l st 282 in go (foldl' (flip (:)) vs vs') 283 (lc + 1) (ma + ma') st' ls 284 285 -- | Check entire CFG with taint config. 286 checkCFGWithConfig :: RuntimeConfig -> TaintConfig 287 -> Text -> CFG -> AuditResult 288 checkCFGWithConfig rt tcfg sym cfg = 289 let inStates = runDataflowWithConfig rt tcfg cfg 290 nBlocks = cfgBlockCount cfg 291 baseState = initTaintState rt 292 in mconcat 293 [ fst (checkBlock rt blockSym inState 294 (bbLines bb)) 295 | idx <- [0..nBlocks-1] 296 , let bb = indexBlock cfg idx 297 blockSym = 298 fromMaybe sym (blockFunction cfg idx) 299 inState = 300 IM.findWithDefault baseState 301 idx inStates 302 ] 303 304 -- | Check entire CFG with inter-procedural analysis 305 -- and taint config. Uses whole-file dataflow with 306 -- summaries to properly propagate taint across tail 307 -- call boundaries. 308 checkCFGInterProcWithConfig 309 :: RuntimeConfig -> TaintConfig -> Text -> CFG 310 -> AuditResult 311 checkCFGInterProcWithConfig rt tcfg sym cfg = 312 let summaries = runInterProcWithConfig rt tcfg cfg 313 inStates = 314 runDataflowWithConfigAndSummaries rt tcfg 315 summaries cfg 316 nBlocks = cfgBlockCount cfg 317 baseState = initTaintState rt 318 in mconcat 319 [ fst (checkBlockWithSummary rt blockSym 320 summaries inState (bbLines bb)) 321 | idx <- [0..nBlocks-1] 322 , let bb = indexBlock cfg idx 323 blockSym = 324 fromMaybe sym (blockFunction cfg idx) 325 inState = 326 IM.findWithDefault baseState 327 idx inStates 328 ]