Abstract
<title>Abstract</title> <p>Proofs of execution let a verifier trust that a low-end embedded device ran a function correctly, underpinning defenses against data poisoning. Stateful proofs of execution on commodity Arm TrustZone-M guarantee that a successful proof certifies its output was produced over authentic, unmodified state under a fully compromised non-secure world; we study it through a published, prototyped instance, SLAPP (IEEE TIFS 2025). That guarantee rests on a state-authenticity property (P4) whose argument reduces state tampering to program-memory modification, caught by the measurement. The reduction is unsound: the measurement enforces code integrity, not state authenticity, and TrustZone-M's address-based isolation binds only the CPU. A non-secure DMA controller, programmable by default, writes the attested state in data memory without touching program memory. On SLAPP's reference board, within its adversary model, a software adversary corrupts the attested state inside the check-then-commit window, and our prototype accepts a proof over adversary-chosen state against the attack image's own reference; the state-tampering refutation itself is reference-independent, and we scope the code-identical case separately. Because SLAPP's atomicity disables CPU interrupts, which does not constrain a bus master, the corruption succeeds with interrupts disabled, reaching the strict, as-published configuration. We show why the platform's three isolation facilities fail, and give a lightweight, register-validated mitigation using the DMA controller's own per-channel security. The gap and its fix share a principle applying to any TrustZone-M proof of execution over mutable state: authenticity must be mediated against every bus master that can write it, not only the CPU.</p>