commit 191611b72312b0990f0e4488c2c61ce47bcd1c3a
parent f1f3facd8d49e27fc1f2d90ed222d42025838043
Author: Jared Tobin <jared@jtobin.io>
Date: Thu, 26 Feb 2026 17:14:54 +0400
docs: modernize README with current features
Update documentation to cover:
- Taint analysis with inter-procedural support
- Taint configuration files (secret, public, secret_pointee, STG slots)
- NCT scan mode with symbol-focused analysis
- GHC runtime filtering
- Utility commands (list-symbols, filter, zsymbol)
- Updated limitations section
Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com>
Diffstat:
| M | README.md | | | 149 | +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++-------------- |
1 file changed, 124 insertions(+), 25 deletions(-)
diff --git a/README.md b/README.md
@@ -3,23 +3,27 @@
A Haskell tool for static analysis of GHC-generated AArch64 assembly,
-focused on constant-time memory access auditing for cryptographic code.
+focused on constant-time auditing for cryptographic code.
## Overview
-ppad-auditor parses AArch64 assembly and performs taint analysis to
-identify memory accesses that may leak secret data through
-timing side-channels. It flags loads and stores where:
+ppad-auditor provides two analysis modes:
-- The base register may contain secret-derived data
-- An index register may contain secret-derived data
+1. **Taint analysis** (default): Tracks how secret data flows through
+ registers and memory, flagging loads/stores where the address may
+ depend on secret values (cache timing side-channels).
-The tool assumes GHC's calling convention, where certain registers
-(X19-X22, SP) are treated as public (stack/heap pointers), and tracks
-how taint propagates through arithmetic and data movement instructions
-across basic blocks.
+2. **NCT scan** (`--scan-nct`): Identifies non-constant-time
+ instructions (variable-time division, conditional branches, etc.)
+ that may leak secrets through execution timing.
-## Usage
+The tool understands GHC's calling conventions, treating registers like
+X19-X22 and SP as public pointers, and tracking taint propagation
+through arithmetic, data movement, and function calls.
+
+## Taint Analysis
+
+Basic usage:
```
$ auditor -i input.s
@@ -36,38 +40,133 @@ Memory accesses: 37
Violations: 2
```
-Use `-q` for quiet mode (violations only), `-j` for JSON output, or
-`-p` for inter-procedural analysis (computes function summaries).
+### Inter-procedural Analysis
-## Limitations
+Use `-p` to enable inter-procedural analysis, which computes function
+summaries and propagates taint across call boundaries:
+
+```
+$ auditor -i input.s -p
+```
+
+### Taint Configuration
+
+Seed specific registers or STG stack slots as secret using a JSON
+config file:
+
+```json
+{
+ "_my_function_info$def": {
+ "secret": ["X0", "X1"],
+ "public": ["X2"],
+ "secret_pointee": ["X3"],
+ "stg_secret": [8, 16],
+ "stg_public": [24]
+ }
+}
+```
+
+- `secret`: Registers containing secret scalar values
+- `public`: Registers to mark as public
+- `secret_pointee`: Registers that are public pointers to secret data
+ (loads through them produce secret values)
+- `stg_secret` / `stg_public`: STG stack slot offsets (X20-relative)
+
+Apply with:
+
+```
+$ auditor -i input.s -p --taint-config config.json
+```
+
+### Display Options
+
+- `-u`: Show unknown violations (only secret violations shown by
+ default)
+- `-q`: Quiet mode (violations only, no summary)
+- `-j`: JSON output format
+- `--assume-stg-private`: Treat untracked STG stack slots as private
+ (default assumes they're public closure pointers)
+
+## NCT Scan
+
+Scan for non-constant-time instructions without taint analysis:
+
+```
+$ auditor -i input.s --scan-nct
+```
+
+This identifies:
+- Variable-time arithmetic (udiv, sdiv without DIT)
+- Conditional branches (b.cond, cbz, cbnz, tbz, tbnz)
+- Register-indexed memory accesses
+
+### Symbol-Focused Scanning
+
+Analyze a specific function and its callees:
-This is an early-stage tool with known limitations:
+```
+$ auditor -i input.s --scan-nct --symbol _my_func_info
+```
+
+Or use human-readable z-encoded symbols:
+
+```
+$ auditor -i input.s --scan-nct --zsymbol "pkg-1.0:Module.Name:function"
+```
+
+Use `-c` to show callers instead of callees (reverse reachability).
+
+### GHC Runtime Filtering
+
+GHC runtime patterns (heap checks, stack checks, closure evaluation)
+are hidden by default. Show them with:
+
+```
+$ auditor -i input.s --scan-nct --show-ghc-runtime
+```
+
+## Utility Commands
+
+List all function symbols:
+
+```
+$ auditor -i input.s --list-symbols
+```
+
+Filter symbols by pattern:
+
+```
+$ auditor -i input.s --list-symbols --filter "multiply"
+```
+
+## Limitations
-- **No inter-procedural analysis**: Function calls reset taint state
- for caller-saved registers; callees are analyzed independently even
- when defined in the same file
-- **Conservative**: Unknown taint is treated as potentially secret
+- **Conservative analysis**: Unknown taint is treated as potentially
+ secret, which may cause over-reporting
+- **GHC-specific**: Assumes GHC's STG calling convention and register
+ usage; may not work well with other compilers
+- **No alias analysis**: Heap accesses use coarse tracking; complex
+ pointer aliasing may cause false positives/negatives
-These limitations mean the tool may over-report violations. Manual
-review of flagged accesses is required.
+Manual review of flagged accesses is recommended.
## Development
-You'll require [Nix][nixos] with [flake][flake] support enabled. Enter a
-development shell with:
+Requires [Nix][nixos] with [flake][flake] support. Enter a development
+shell:
```
$ nix develop
```
-Then build and test:
+Build and test:
```
$ cabal build
$ cabal test
```
-To audit some assembly:
+Audit some assembly:
```
$ cabal run auditor -- -i path/to/file.s
