Contract.hs (14795B)
1 {-# OPTIONS_HADDOCK prune #-} 2 {-# LANGUAGE OverloadedStrings #-} 3 4 -- | 5 -- Module: Vestigia.Contract 6 -- Copyright: (c) 2026 Jared Tobin 7 -- License: MIT 8 -- Maintainer: Jared Tobin <jared@ppad.tech> 9 -- 10 -- An ISA's data-independent-timing contract, and what it makes of 11 -- each instruction of an object: one it covers takes a time 12 -- independent of its data; one it does not, run on operands that 13 -- depend on the secret, is outside the contract; and a division is 14 -- variable-time on either ISA. Control flow and system instructions 15 -- are left to the comparison of what ran. 16 -- 17 -- An object is read through LLVM's disassembler (@llvm-objdump@), in 18 -- Intel syntax on x86_64. On AArch64 an instruction is matched by its 19 -- encoding against Arm's own ('Vestigia.Contract.Arm'), its source 20 -- registers read off the fields the encoding names. On x86_64 it is 21 -- matched by its mnemonic and opcode byte against Intel's list 22 -- ('Vestigia.Contract.Intel'), its source registers read off its 23 -- operands: every register operand outside a memory reference, but 24 -- the first where the instruction only writes it, and the registers 25 -- some instructions read without naming. 26 -- 27 -- What is outside the contract and reads data becomes the watch 28 -- list the QEMU plugin is given: each such instruction, by its 29 -- address in its object, with the registers to fingerprint before it 30 -- runs, as the plugin fingerprints a division's operands. 31 32 module Vestigia.Contract ( 33 Contract(..) 34 , contractName 35 , contractSource 36 , contractIsa 37 , readContract 38 , Line(..) 39 , readDisassembly 40 , Register(..) 41 , Verdict(..) 42 , classify 43 , watchSection 44 ) where 45 46 import Data.Bits (popCount, shiftR, testBit, (.&.)) 47 import Data.Char (isHexDigit) 48 import qualified Data.List as L 49 import qualified Data.Map.Strict as M 50 import qualified Data.Set as S 51 import qualified Data.Text as T 52 import Data.Word (Word32, Word8) 53 import Numeric (readHex, showHex) 54 55 import qualified Vestigia.Contract.Arm as Arm 56 import qualified Vestigia.Contract.Intel as Intel 57 import Vestigia.Contract.Types 58 59 -- | A data-independent-timing contract: Arm's @PSTATE.DIT@, or 60 -- Intel's DOITM. 61 data Contract = 62 ArmDit 63 | IntelDoitm 64 deriving (Eq, Show) 65 66 contractName :: Contract -> T.Text 67 contractName c = case c of 68 ArmDit -> "arm-dit" 69 IntelDoitm -> "intel-doitm" 70 71 -- | The release of the vendor's own statement the table transcribes. 72 contractSource :: Contract -> T.Text 73 contractSource c = case c of 74 ArmDit -> "Arm A64 ISA XML, 2022-12" 75 IntelDoitm -> "Intel 768547, Table 1, 2026-02-23" 76 77 -- | The ISA a contract speaks to, as QEMU names it. 78 contractIsa :: Contract -> String 79 contractIsa c = case c of 80 ArmDit -> "aarch64" 81 IntelDoitm -> "x86_64" 82 83 readContract :: T.Text -> Maybe Contract 84 readContract t = case t of 85 "arm-dit" -> Just ArmDit 86 "intel-doitm" -> Just IntelDoitm 87 _ -> Nothing 88 89 -- | One instruction as the disassembler prints it: its address in 90 -- the object, its raw form (an AArch64 word, or x86_64's bytes), 91 -- any prefixes, its mnemonic, and its operands. 92 data Line = Line { 93 lnAddress :: !Integer 94 , lnRaw :: ![Integer] 95 , lnPrefixes :: ![T.Text] 96 , lnMnemonic :: !T.Text 97 , lnOperands :: !T.Text 98 } deriving (Eq, Show) 99 100 -- | The instructions of @llvm-objdump@'s disassembly; everything 101 -- else it prints (headers, symbols, elided runs) is passed over. 102 readDisassembly :: T.Text -> [Line] 103 readDisassembly = concatMap line . T.lines 104 where 105 line l = case T.breakOn ":" (T.stripStart l) of 106 (a, rest) 107 | not (T.null a), T.all isHexDigit a 108 , Just body <- T.stripPrefix ":" rest 109 , [ (addr, "") ] <- readHex (T.unpack a) 110 , (raw, text) <- T.breakOn "\t" body 111 , Just ws <- traverse hexToken (T.words raw) 112 , not (null ws) -> 113 case filter (not . T.null) 114 (fmap T.strip (T.splitOn "\t" text)) of 115 [] -> [] 116 fs -> let (ps, rest') = L.span (`S.member` prefixes) fs 117 in case rest' of 118 (m : ops) -> [ Line addr ws ps m 119 (uncomment (T.unwords ops)) ] 120 [] -> [] 121 _ -> [] 122 hexToken w 123 | T.all isHexDigit w, [ (v, "") ] <- readHex (T.unpack w) = Just v 124 | otherwise = Nothing 125 -- the disassembler's annotations, x86_64's after " # " and 126 -- AArch64's after " //": a target or a literal, never an operand 127 -- (an AArch64 immediate is "#" with no space after it) 128 uncomment t = 129 T.stripEnd (fst (T.breakOn " //" (fst (T.breakOn " # " t)))) 130 131 -- prefixes the disassembler prints as fields of their own 132 prefixes :: S.Set T.Text 133 prefixes = S.fromList 134 [ "lock", "rep", "repe", "repz", "repne", "repnz", "data16", "data32" 135 , "addr32", "notrack", "bnd", "xacquire", "xrelease", "cs", "ds" 136 , "es", "fs", "gs", "ss" ] 137 138 -- | A register to fingerprint, as QEMU names it, by the bits read: 139 -- from its low bit, so many of them. 140 data Register = Register { 141 rgName :: !T.Text 142 , rgLow :: !Int 143 , rgWidth :: !Int 144 } deriving (Eq, Ord, Show) 145 146 -- | What a contract makes of an instruction: covered by it; control 147 -- flow or system, or reading no data; an integer division, which 148 -- the plugin reads for itself; or outside the contract, with the 149 -- registers it reads and whether it names memory. 150 data Verdict = 151 Inside 152 | Excluded 153 | Division 154 | Watched ![Register] !Bool 155 deriving (Eq, Show) 156 157 -- | Classify one instruction under a contract. 158 classify :: Contract -> Line -> Verdict 159 classify c l = case c of 160 ArmDit -> case lnRaw l of 161 [ w ] | w >= 0, w < 2 ^ (32 :: Int) -> arm (fromInteger w) l 162 _ -> Excluded 163 IntelDoitm -> intel l 164 165 -- AArch64 --------------------------------------------------------- 166 167 arm :: Word32 -> Line -> Verdict 168 arm w l = case best of 169 Nothing -> Excluded 170 Just e 171 | any (`T.isPrefixOf` enName e) [ "UDIV_", "SDIV_" ] -> Division 172 | otherwise -> case enStatus e of 173 Covered -> Inside 174 Control -> Excluded 175 Outside ops -> case concatMap (register w) ops of 176 [] | not memory -> Excluded 177 rs -> Watched (L.nub rs) memory 178 where 179 memory = "[" `T.isInfixOf` lnOperands l 180 candidates = M.findWithDefault [] (bucket w) armIndex 181 best = case [ e | e <- candidates, w .&. enMask e == enValue e ] of 182 [] -> Nothing 183 es -> Just (L.maximumBy (\a b -> compare (fixed a) (fixed b)) es) 184 fixed e = popCount (enMask e) 185 186 -- an encoding's group, bits 28 to 25 187 bucket :: Word32 -> Word32 188 bucket w = (w `shiftR` 25) .&. 0xf 189 190 -- the encodings by every group their fixed bits allow 191 armIndex :: M.Map Word32 [Encoding] 192 armIndex = M.fromListWith (flip (<>)) 193 [ (b, [ e ]) 194 | e <- Arm.encodings 195 , b <- [ 0 .. 15 ] 196 , b .&. bucket (enMask e) == bucket (enValue e) ] 197 198 register :: Word32 -> (Int, Operand) -> [Register] 199 register w (lsb, op) = 200 let n = fromIntegral ((w `shiftR` lsb) .&. 31) :: Int 201 x = "x" <> T.pack (show n) 202 v = "v" <> T.pack (show n) 203 in case op of 204 OpX | n == 31 -> [] 205 | otherwise -> [ Register x 0 64 ] 206 OpXSp | n == 31 -> [ Register "sp" 0 64 ] 207 | otherwise -> [ Register x 0 64 ] 208 OpW | n == 31 -> [] 209 | otherwise -> [ Register x 0 32 ] 210 OpWSp | n == 31 -> [ Register "sp" 0 32 ] 211 | otherwise -> [ Register x 0 32 ] 212 OpQ -> [ Register v 0 128 ] 213 OpD -> [ Register v 0 64 ] 214 OpS -> [ Register v 0 32 ] 215 OpH -> [ Register v 0 16 ] 216 OpB -> [ Register v 0 8 ] 217 OpV -> [ Register v 0 (if testBit w 30 then 128 else 64) ] 218 OpVWhole -> [ Register v 0 128 ] 219 220 -- x86_64 ---------------------------------------------------------- 221 222 intel :: Line -> Verdict 223 intel l 224 | m `S.member` control || "J" `T.isPrefixOf` m = Excluded 225 | m == "DIV" || m == "IDIV" = Division 226 | Just op <- opcode (lnRaw l) 227 , (name, op) `S.member` intelRows = Inside 228 | null sources && not memory = Excluded 229 | otherwise = Watched (L.nub sources) memory 230 where 231 m = mnemonic l 232 -- a repeat prefix names a string instruction's row; on any other 233 -- it does nothing 234 name 235 | any (`elem` [ "rep", "repe", "repz", "repne", "repnz" ]) 236 (lnPrefixes l) 237 , any (`T.isPrefixOf` m) 238 [ "MOVS", "STOS", "LODS", "CMPS", "SCAS", "INS", "OUTS" ] = 239 "REP_" <> m 240 | otherwise = m 241 operands = splitOperands (lnOperands l) 242 memory = any ("[" `T.isInfixOf`) operands 243 named = [ r | o <- operands, not ("[" `T.isInfixOf` o) 244 , Just r <- [ M.lookup (bare o) intelRegisters ] ] 245 explicit = case operands of 246 (o : _) | writesOnly m, not ("[" `T.isInfixOf` o) -> drop 1 named 247 _ -> named 248 sources = explicit <> M.findWithDefault [] m implicit 249 250 intelRows :: S.Set (T.Text, Word8) 251 intelRows = S.fromList Intel.instructions 252 253 -- the mnemonic as Intel's list spells it: upper case, a condition by 254 -- its list name, a 64-bit immediate move as a move 255 mnemonic :: Line -> T.Text 256 mnemonic l = 257 let m = T.toUpper (lnMnemonic l) 258 in case m of 259 "MOVABS" -> "MOV" 260 _ -> case [ p <> c' | p <- [ "CMOV", "SET" ] 261 , Just c <- [ T.stripPrefix p m ] 262 , Just c' <- [ M.lookup c conditions ] ] of 263 (n : _) -> n 264 [] -> m 265 266 conditions :: M.Map T.Text T.Text 267 conditions = M.fromList 268 [ ("O", "O"), ("NO", "NO"), ("B", "B"), ("C", "B"), ("NAE", "B") 269 , ("NB", "NB"), ("AE", "NB"), ("NC", "NB"), ("Z", "Z"), ("E", "Z") 270 , ("NZ", "NZ"), ("NE", "NZ"), ("BE", "BE"), ("NA", "BE") 271 , ("NBE", "NBE"), ("A", "NBE"), ("S", "S"), ("NS", "NS"), ("P", "P") 272 , ("PE", "P"), ("NP", "NP"), ("PO", "NP"), ("L", "L"), ("NGE", "L") 273 , ("NL", "NL"), ("GE", "NL"), ("LE", "LE"), ("NG", "LE") 274 , ("NLE", "NLE"), ("G", "NLE") ] 275 276 -- control flow, system, and instructions that read no data 277 control :: S.Set T.Text 278 control = S.fromList 279 [ "CALL", "RET", "LOOP", "LOOPE", "LOOPNE", "SYSCALL", "SYSENTER" 280 , "INT", "INT3", "INTO", "UD1", "UD2", "HLT", "NOP", "PAUSE" 281 , "ENDBR32", "ENDBR64", "LFENCE", "MFENCE", "SFENCE", "CPUID" 282 , "RDTSC", "RDTSCP", "XGETBV", "RDRAND", "RDSEED", "ENTER", "LEAVE" 283 , "PREFETCHT0", "PREFETCHT1", "PREFETCHT2", "PREFETCHNTA" 284 , "PREFETCHW", "CLFLUSH", "CLFLUSHOPT" ] 285 286 -- instructions that write their first operand without reading it 287 writesOnly :: T.Text -> Bool 288 writesOnly m = 289 ("V" `T.isPrefixOf` m && m /= "VZEROUPPER" && m /= "VZEROALL") 290 || "MOV" `T.isPrefixOf` m 291 || "CVT" `T.isPrefixOf` m 292 || any (`T.isPrefixOf` m) [ "SQRT", "RSQRT", "RCP" ] 293 || m `elem` [ "POPCNT", "LZCNT", "TZCNT", "PDEP", "PEXT", "BZHI" 294 , "BEXTR", "BLSI", "BLSR", "BLSMSK", "SARX", "LEA" ] 295 296 -- registers read without being named 297 implicit :: M.Map T.Text [Register] 298 implicit = M.fromList 299 [ ("CBW", [ Register "rax" 0 8 ]), ("CWDE", [ Register "rax" 0 16 ]) 300 , ("CDQE", [ Register "rax" 0 32 ]), ("CWD", [ Register "rax" 0 16 ]) 301 , ("CDQ", [ Register "rax" 0 32 ]), ("CQO", [ Register "rax" 0 64 ]) 302 , ("SAHF", [ Register "rax" 8 8 ]) 303 , ("CMPXCHG", [ Register "rax" 0 64 ]) 304 , ("CMPXCHG8B", fmap (\r -> Register r 0 32) 305 [ "rax", "rdx", "rbx", "rcx" ]) 306 , ("CMPXCHG16B", fmap (\r -> Register r 0 64) 307 [ "rax", "rdx", "rbx", "rcx" ]) ] 308 309 -- an operand less its masking and broadcast decorations 310 bare :: T.Text -> T.Text 311 bare = T.strip . T.takeWhile (/= '{') 312 313 -- operands, split at the commas between them 314 splitOperands :: T.Text -> [T.Text] 315 splitOperands t 316 | T.null (T.strip t) = [] 317 | otherwise = fmap T.strip (go 0 "" (T.unpack t)) 318 where 319 go :: Int -> String -> String -> [T.Text] 320 go _ acc [] = [ T.pack (reverse acc) ] 321 go d acc (ch : rest) = case ch of 322 '[' -> go (d + 1) (ch : acc) rest 323 ']' -> go (d - 1) (ch : acc) rest 324 ',' | d == 0 -> T.pack (reverse acc) : go d "" rest 325 _ -> go d (ch : acc) rest 326 327 -- the general and vector registers QEMU exposes, by their names in 328 -- Intel syntax: a wide vector by its low 128 bits, which is all of 329 -- it QEMU names 330 intelRegisters :: M.Map T.Text Register 331 intelRegisters = M.fromList $ 332 concat 333 [ [ (r64, Register r64 0 64), (r32, Register r64 0 32) 334 , (r16, Register r64 0 16), (r8, Register r64 0 8) ] 335 | (r64, r32, r16, r8) <- 336 [ ("rax", "eax", "ax", "al"), ("rbx", "ebx", "bx", "bl") 337 , ("rcx", "ecx", "cx", "cl"), ("rdx", "edx", "dx", "dl") 338 , ("rsi", "esi", "si", "sil"), ("rdi", "edi", "di", "dil") 339 , ("rbp", "ebp", "bp", "bpl"), ("rsp", "esp", "sp", "spl") ] 340 <> [ (n, n <> "d", n <> "w", n <> "b") 341 | k <- [ 8 .. 15 :: Int ], let n = "r" <> T.pack (show k) ] ] 342 <> [ (h, Register r 8 8) 343 | (h, r) <- [ ("ah", "rax"), ("bh", "rbx"), ("ch", "rcx") 344 , ("dh", "rdx") ] ] 345 <> [ (p <> T.pack (show k), Register ("xmm" <> T.pack (show k)) 0 128) 346 | p <- [ "xmm", "ymm", "zmm" ], k <- [ 0 .. 15 :: Int ] ] 347 348 -- the last opcode byte, past the prefixes, a REX, any VEX or EVEX 349 -- payload, and the escape bytes 350 opcode :: [Integer] -> Maybe Word8 351 opcode bs = fmap fromInteger (go (dropWhile legacy bs)) 352 where 353 legacy b = b `elem` [ 0x66, 0x67, 0xf0, 0xf2, 0xf3, 0x2e, 0x36 354 , 0x3e, 0x26, 0x64, 0x65 ] 355 go xs = case xs of 356 (b : rest) | b >= 0x40 && b <= 0x4f -> escaped rest 357 (0xd5 : _ : rest) -> at 0 rest 358 _ -> escaped xs 359 escaped xs = case xs of 360 (0xc5 : rest) -> at 1 rest 361 (0xc4 : rest) -> at 2 rest 362 (0x62 : rest) -> at 3 rest 363 (0x0f : 0x38 : rest) -> at 0 rest 364 (0x0f : 0x3a : rest) -> at 0 rest 365 (0x0f : rest) -> at 0 rest 366 _ -> at 0 xs 367 at k xs = case drop k xs of 368 (b : _) -> Just b 369 [] -> Nothing 370 371 -- the watch list ---------------------------------------------------- 372 373 -- | The plugin's watch list for one object, at its path: an @O@ line 374 -- naming it, then a @D@ line per division and a @U@ line per 375 -- instruction outside the contract, each with its address and its 376 -- text (a @U@ line with whether it names memory and the registers 377 -- it reads, each as name:low:width, before the text). 378 watchSection :: Contract -> FilePath -> [Line] -> T.Text 379 watchSection c path ls = T.unlines $ 380 ("O " <> T.pack path) 381 : concatMap entry ls 382 where 383 entry l = case classify c l of 384 Division -> [ "D " <> hex (lnAddress l) <> " " <> text l ] 385 Watched rs memory -> 386 [ T.unwords $ 387 [ "U", hex (lnAddress l), if memory then "1" else "0" 388 , T.pack (show (length rs)) ] 389 <> [ rgName r <> ":" <> T.pack (show (rgLow r)) <> ":" 390 <> T.pack (show (rgWidth r)) | r <- rs ] 391 <> [ text l ] ] 392 _ -> [] 393 text l = T.unwords (filter (not . T.null) 394 (lnPrefixes l <> [ lnMnemonic l, lnOperands l ])) 395 hex n = T.pack (showHex n "")