ppad-auditor

A research-grade Haskell tool for static analysis of AArch64 assembly, focused on constant-time auditing for cryptographic code.

Overview

ppad-auditor provides two analysis modes:

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).

2. NCT scan (--scan-nct): Identifies non-constant-time instructions (variable-time division, conditional branches, etc.) that may leak secrets through execution timing.

The tool is parameterised over a runtime configuration, so it can adapt to different compilers and calling conventions. The default runtime (haskell) understands GHC's STG calling conventions, treating registers like X19-X22 and SP as public pointers. A generic runtime is also available as a baseline for C, Rust, or Go code.

Taint Analysis

Basic usage (defaults to Haskell/GHC runtime):

$ auditor -i input.s

Sample output:

LBB0_4:42: unknown base register x8
Lloh5:62: unknown base register x9

Lines checked:    202
Memory accesses:  37
Violations:       2

Runtime Selection

Use --runtime to select the target runtime:

$ auditor -i input.s --runtime haskell   # default
$ auditor -i input.s --runtime generic   # C/Rust/Go baseline

The haskell runtime configures GHC's STG register conventions, secondary stack tracking (X20), pointer untagging masks, and runtime pattern filtering. The generic runtime uses only hardware stack/frame pointers and zero registers as public roots, with no secondary stack or untagging heuristics.

Inter-procedural Analysis

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 secondary stack slots as secret using a JSON config file:

{
  "_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: Secondary stack slot offsets (X20-relative when using the haskell runtime)

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-secondary-private: Treat untracked secondary 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:

$ auditor -i input.s --scan-nct --symbol _my_func_info

Or use human-readable z-encoded symbols (Haskell runtime only):

$ auditor -i input.s --scan-nct \
    --zsymbol "pkg-1.0:Module.Name:function"

Use -c to show callers instead of callees (reverse reachability).

Runtime Pattern Filtering

Runtime-specific patterns (heap checks, stack checks, closure evaluation) are hidden by default. Show them with:

$ auditor -i input.s --scan-nct --show-runtime-patterns

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

• Conservative analysis: Unknown taint is treated as potentially secret, which may cause over-reporting
• No alias analysis: Heap accesses use coarse tracking; complex pointer aliasing may cause false positives/negatives

Manual review of flagged accesses is recommended.

Development

Requires Nix with flake support. Enter a development shell:

$ nix develop

Build and test:

$ cabal build
$ cabal test

Audit some assembly:

$ cabal run auditor -- -i path/to/file.s