auditor

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

ARCH17.md (1621B)

      1 # ARCH17: Heap/Memory Taint Propagation
      2 
      3 ## Goal
      4 
      5 Propagate taint and kind information through heap/memory loads and
      6 stores so secret values loaded from heap objects can influence address
      7 checks (e.g., secret-indexed table lookups).
      8 
      9 ## Scope
     10 
     11 Stage 1 (coarse heap bucket):
     12 - Track a single heap taint/provenance/kind bucket for non-stack memory.
     13 - Stores to non-stack memory join into the heap bucket.
     14 - Loads from non-stack memory read from the heap bucket.
     15 
     16 Stage 2 (refined base+offset tracking):
     17 - Track taint/kind for addresses of the form `[base, #imm]` when `base`
     18   is a public pointer (or provably public). Use `(base, imm)` as key.
     19 - Fallback to coarse heap bucket for other forms.
     20 
     21 ## Rationale
     22 
     23 Current analysis treats non-stack loads as Unknown, preventing secrets
     24 from flowing into index calculations. A shadow heap model enables secret
     25 propagation without full alias analysis.
     26 
     27 ## Design
     28 
     29 ### Coarse Heap Bucket (Stage 1)
     30 
     31 - Add `tsHeapTaint :: Taint`, `tsHeapProv :: Provenance`,
     32   `tsHeapKind :: RegKind`.
     33 - On store to non-stack address: `heap := join heap (src)`.
     34 - On load from non-stack address: `dst := heap` (unless public root).
     35 
     36 ### Refined Map (Stage 2)
     37 
     38 - Add `tsHeapSlots :: Map (Reg, Int) (Taint, Provenance, RegKind)` for
     39   `[base, #imm]` with `base` KindPtr and public provenance.
     40 - Stores to such addresses update the slot; loads read from it.
     41 - Other heap accesses join into the coarse bucket.
     42 
     43 ## Risks
     44 
     45 - Coarse bucket may over-taint (false positives).
     46 - Refined map needs clear rules for when base is considered public.
     47 - Aliasing is not solved; this is a conservative approximation.