README.md (4599B)
1 # ppad-auditor 2 3  4 5 A research-grade Haskell tool for static analysis of AArch64 assembly, 6 focused on constant-time auditing for cryptographic code. 7 8 ## Overview 9 10 ppad-auditor provides two analysis modes: 11 12 1. **Taint analysis** (default): Tracks how secret data flows 13 through registers and memory, flagging loads/stores where the 14 address may depend on secret values (cache timing 15 side-channels). 16 17 2. **NCT scan** (`--scan-nct`): Identifies non-constant-time 18 instructions (variable-time division, conditional branches, 19 etc.) that may leak secrets through execution timing. 20 21 The tool is parameterised over a runtime configuration, so it can 22 adapt to different compilers and calling conventions. The default 23 runtime (`haskell`) understands GHC's STG calling conventions, 24 treating registers like X19-X22 and SP as public pointers. A 25 `generic` runtime is also available as a baseline for C, Rust, or 26 Go code. 27 28 ## Taint Analysis 29 30 Basic usage (defaults to Haskell/GHC runtime): 31 32 ``` 33 $ auditor -i input.s 34 ``` 35 36 Sample output: 37 38 ``` 39 LBB0_4:42: unknown base register x8 40 Lloh5:62: unknown base register x9 41 42 Lines checked: 202 43 Memory accesses: 37 44 Violations: 2 45 ``` 46 47 ### Runtime Selection 48 49 Use `--runtime` to select the target runtime: 50 51 ``` 52 $ auditor -i input.s --runtime haskell # default 53 $ auditor -i input.s --runtime generic # C/Rust/Go baseline 54 ``` 55 56 The `haskell` runtime configures GHC's STG register conventions, 57 secondary stack tracking (X20), pointer untagging masks, and 58 runtime pattern filtering. The `generic` runtime uses only 59 hardware stack/frame pointers and zero registers as public roots, 60 with no secondary stack or untagging heuristics. 61 62 ### Inter-procedural Analysis 63 64 Use `-p` to enable inter-procedural analysis, which computes 65 function summaries and propagates taint across call boundaries: 66 67 ``` 68 $ auditor -i input.s -p 69 ``` 70 71 ### Taint Configuration 72 73 Seed specific registers or secondary stack slots as secret using a 74 JSON config file: 75 76 ```json 77 { 78 "_my_function_info$def": { 79 "secret": ["X0", "X1"], 80 "public": ["X2"], 81 "secret_pointee": ["X3"], 82 "stg_secret": [8, 16], 83 "stg_public": [24] 84 } 85 } 86 ``` 87 88 - `secret`: Registers containing secret scalar values 89 - `public`: Registers to mark as public 90 - `secret_pointee`: Registers that are public pointers to secret 91 data (loads through them produce secret values) 92 - `stg_secret` / `stg_public`: Secondary stack slot offsets 93 (X20-relative when using the `haskell` runtime) 94 95 Apply with: 96 97 ``` 98 $ auditor -i input.s -p --taint-config config.json 99 ``` 100 101 ### Display Options 102 103 - `-u`: Show unknown violations (only secret violations shown by 104 default) 105 - `-q`: Quiet mode (violations only, no summary) 106 - `-j`: JSON output format 107 - `--assume-secondary-private`: Treat untracked secondary stack 108 slots as private (default assumes they're public closure 109 pointers) 110 111 ## NCT Scan 112 113 Scan for non-constant-time instructions without taint analysis: 114 115 ``` 116 $ auditor -i input.s --scan-nct 117 ``` 118 119 This identifies: 120 - Variable-time arithmetic (udiv, sdiv without DIT) 121 - Conditional branches (b.cond, cbz, cbnz, tbz, tbnz) 122 - Register-indexed memory accesses 123 124 ### Symbol-Focused Scanning 125 126 Analyze a specific function and its callees: 127 128 ``` 129 $ auditor -i input.s --scan-nct --symbol _my_func_info 130 ``` 131 132 Or use human-readable z-encoded symbols (Haskell runtime only): 133 134 ``` 135 $ auditor -i input.s --scan-nct \ 136 --zsymbol "pkg-1.0:Module.Name:function" 137 ``` 138 139 Use `-c` to show callers instead of callees (reverse 140 reachability). 141 142 ### Runtime Pattern Filtering 143 144 Runtime-specific patterns (heap checks, stack checks, closure 145 evaluation) are hidden by default. Show them with: 146 147 ``` 148 $ auditor -i input.s --scan-nct --show-runtime-patterns 149 ``` 150 151 ## Utility Commands 152 153 List all function symbols: 154 155 ``` 156 $ auditor -i input.s --list-symbols 157 ``` 158 159 Filter symbols by pattern: 160 161 ``` 162 $ auditor -i input.s --list-symbols --filter "multiply" 163 ``` 164 165 ## Limitations 166 167 - **Conservative analysis**: Unknown taint is treated as 168 potentially secret, which may cause over-reporting 169 - **No alias analysis**: Heap accesses use coarse tracking; 170 complex pointer aliasing may cause false positives/negatives 171 172 Manual review of flagged accesses is recommended. 173 174 ## Development 175 176 Requires [Nix][nixos] with [flake][flake] support. Enter a 177 development shell: 178 179 ``` 180 $ nix develop 181 ``` 182 183 Build and test: 184 185 ``` 186 $ cabal build 187 $ cabal test 188 ``` 189 190 Audit some assembly: 191 192 ``` 193 $ cabal run auditor -- -i path/to/file.s 194 ``` 195 196 [nixos]: https://nixos.org/ 197 [flake]: https://nixos.org/manual/nix/unstable/command-ref/new-cli/nix3-flake.html