auditor

An aarch64 constant-time memory access auditing tool.
git clone git://git.ppad.tech/auditor.git
Log | Files | Refs | README | LICENSE

IMPL0.md (2615B)

      1 # IMPL0: AArch64 ASM Constant-Time Memory Access Audit Tool
      2 
      3 ## Goal
      4 
      5 Implement a Haskell (GHC 9.10.3) prototype static analyzer for
      6 AArch64 GHC+LLVM assembly that enforces a strict memory-access policy
      7 (public base register + constant offset or whitelisted addressing).
      8 
      9 ## Inputs and References
     10 
     11 - Model project structure, flake layout, and cabal style after
     12   `../sha256/flake.nix` and `../sha256/ppad-sha256.cabal`.
     13 - Figure out the register map to use for GHC 9.10.3 by locating the
     14   public AArch64 calling-convention details in GHC headers.
     15 
     16 ## Implementation Steps
     17 
     18 1) Scaffold project layout
     19 - Mirror ppad project structure (lib/, test/, bench/, etc.).
     20 - Draft `flake.nix` patterned after `../sha256/flake.nix`, tailored to
     21   this tool (GHC 9.10.3, LLVM 19, cabal).
     22 - Draft the `.cabal` file patterned after `../sha256/ppad-sha256.cabal`.
     23 
     24 2) Register map research (GHC 9.10.3)
     25 - Locate the AArch64 calling convention definitions in GHC source,
     26   likely in RTS headers or codegen headers (e.g. `rts/include/` or
     27   `compiler/`), and confirm register roles for:
     28   - STG stack pointer, heap pointer, TLS, base reg, etc.
     29 - Produce a concrete register whitelist and document it in code and
     30   README.
     31 
     32 3) Parser and instruction model
     33 - Implement a minimal assembly tokenizer/parser for AArch64 `.s`.
     34 - Normalize addressing modes into a small sum type.
     35 - Represent labels, instructions, and operands with explicit types.
     36 
     37 4) CFG and dataflow engine
     38 - Build basic blocks and a CFG.
     39 - Implement a simple forward dataflow analysis with a 3-point lattice:
     40   Public | Secret | Unknown.
     41 - Initialize public roots using the GHC register map.
     42 
     43 5) Memory access audit rules
     44 - Check all loads/stores for base/index publicness and constant offset.
     45 - Add a configurable whitelist for safe symbols and addressing patterns.
     46 - Emit structured findings (symbol, line, reason).
     47 
     48 6) CLI and reporting
     49 - Provide a small CLI (input asm path, config path, output format).
     50 - Emit both a human summary and JSON output for automation.
     51 
     52 7) Tests and fixtures
     53 - Create small assembly fixtures with known-good and known-bad accesses.
     54 - Add unit tests for parser, CFG builder, and audit rules.
     55 
     56 ## Deliverables
     57 
     58 - Haskell library with core analysis logic in `lib/`.
     59 - CLI executable in `app/`.
     60 - Initial config file (TOML or YAML) with register map and whitelist.
     61 - Tests under `test/` and minimal fixtures under `test/fixtures/`.
     62 
     63 ## Open Questions
     64 
     65 - Exact GHC 9.10.3 AArch64 register map and public-root definitions.
     66 - Whether to depend on a parsing library (megaparsec) or keep it minimal
     67   with hand-rolled parsing to avoid extra deps.