SPTM/MIE: hardware verification plans for GMMU TLBI race and tag-storage aliasing

docs/SPTM-MIE-27.2.md

@@ -164,6 +164,57 @@ not supply.
   reachable primitive (DART userclient, tag-storage mapping, or hibernation
   image control) and a device session; writing one blind would be guesswork.
 
+## Verification plan — GMMU TLBI completion race
+
+The static delta is real, but exploitability depends on keeping a DART client's
+DMA in flight across an unmap. The test is hardware-only; it is written down here
+so the next session does not have to rediscover the shape.
+
+Target: a disposable 27.0.1 device (vulnerable) and a 27.2 device (control).
+
+Primitive needed: an IOGPU userclient plus IOSurface/metal command buffers. The
+kernel DART and IOGPU kexts are unchanged in 27.2 (IOGPU only gained a
+`systemPagingOff()` timeout diagnostic), so the user-reachable map/unmap path is
+the same on both builds; the fix lives inside SPTM.
+
+Steps:
+
+1. Allocate a page-aligned IOSurface `S`, fill it with a canary, map it through
+   IOGPU, and record its physical pages if the API exposes them.
+2. Submit a long-running GPU write into `S` (a compute shader that keeps writing
+   a pattern for several milliseconds).
+3. While the GPU work is in flight, unmap/free `S` through IOGPU so the DART
+   entry is invalidated. On 27.0.1 the invalidation is not completion-checked.
+4. Immediately allocate a fresh page `P` (user or kernel object) and fill it with
+   a different canary. If the GPU's writes land in `P`, the GMMU entry survived
+   the unmap: a stale DMA write primitive.
+5. Escalate only after step 4 is observed: reuse `P` as a kernel object with a
+   pointer field and use the GPU write to corrupt it.
+
+Success criterion: a write to `P` after `S` was unmapped, reproducible on 27.0.1
+and absent on 27.2. A GPU timeout or a single crash is not success; the canary
+difference is.
+
+Safety: run with the phone's panic log enabled, one stage at a time, and stop on
+the first unexpected kernel panic. The harness must journal the stage before the
+unmap (same pattern as Cinder27's GuardJournal).
+
+## Verification plan — MIE tag storage
+
+The SPTM `MTE tag page containing SK tags` check is unchanged, so a bypass here
+would be a new bug, not a 27.2 regression. It needs a kernel primitive that maps
+tag storage with a caller-influenced physical address (or a dangling tag-storage
+reference). The 27.2 diff does not expose such a primitive. The audit order is:
+
+1. Find the kernel callers of the SPTM tag-storage map/unmap operations (the
+   kernel MTE allocator, `VM_KERN_MEMORY_MTAG`).
+2. Check whether the PA is derived from a user-controlled IOSurface/descriptor.
+3. If yes, attempt an alias (map the same PA at a different address) and see
+   whether the SPTM range check still rejects it.
+4. If the check is bypassed, forge the tag for an SK page and read/write it.
+
+Until step 1 yields a user-influenced PA, this remains a hypothesis.
+
 ## Reproduce
 
 ```bash