Memory wiping and proofs of secure erasure

How it works

Proofs of secure erasure (PoSE), introduced by Perito and Tsudik for low-cost embedded devices, rely on the bounded memory of such devices ². A verifier confirms that a device has erased its memory by having it fill that memory with data the verifier can check ³. Perito and Tsudik found this "particularly well-suited" to secure code update and to secure memory or storage erasure ².

Bursuc et al.'s protocols have three phases ³:

1. Fill. The prover fills its memory. In the simplest version the verifier sends random data; in graph-based versions it sends a short seed, and the device computes a large set of hash-chained labels from it ³.
2. Challenge. The verifier asks for randomly chosen blocks, several times, and times each answer ³.
3. Decide. The verifier accepts only if every answer is correct and arrived within the time bound ³.

The graph construction makes it slow to recompute any missing label, so a device that tried to keep other data must fail the deadline ^{3 5}.

In AI verification, the AI 2040 plan proposes "periodic memory wiping on the inference units (which we think can be done through forced memorization)" ¹. The MIRI system overview describes the same step: incompressible data is loaded until the device is full, and then random samples are challenged ⁴. Amodo Design generates the fill on the device from a verifier seed, following Bursuc et al. ⁵.

Reuter and colleagues specify erasure requirements for Pod-PoComp, a proposed protocol that uses compartmentalization to constrain frontier training ⁹. The developer and auditor agree on a memory target and a bound on state that may survive each wipe. An erasure certificate is valid only if the pod answers a fresh challenge in time, the agreed target is covered, and gateway records show no unexplained restore traffic ⁹.

What it establishes

Amodo Design describes the goal as a verifier ensuring "the prover has fully overwritten its memory, with no information persisted across the wipe" ⁵. Amodo says wipes help to verify the "completeness" of declared workloads ⁵. In the AI 2040 plan they help ensure that the only persisting results are verified inference outputs ¹; see inference-only use.

Wipes limit what can carry over between verification cycles, not what runs between them. The AI 2040 plan therefore pairs them with network taps and partial recomputation (Network taps and certifiers, Sampled inference recomputation) ¹. Amodo notes that all stores must be wiped at the same time, because otherwise "an attacker could simply move the data between the disks" ⁵.

In Pod-PoComp, unwipable state must be attested as fixed and included in the initial commitment, or charged to the residual-state bound R. State restored after a wipe must enter through a gateway. It is charged as uncommitted input unless already included in the initial commitment ⁹. This guarantee depends on the hardware, timing and communication assumptions. The erasure certificate bounds surviving state. The compute bound comes separately from pod capacity and the erasure schedule ⁹.

Unrecorded restore traffic is covered only by an assumed side-channel budget B. A deployment that cannot justify that bound fails the paper's erasure assumption ⁹.

Threat model

• Bounded memory. Perito and Tsudik assume bounded memory and a small read-only memory ².
• Distant helpers. Earlier software protocols assumed the device was isolated during the protocol ³. Bursuc et al. relax this: helpers may exist but must be far enough away that their round-trip times exceed the deadline ³.
• Round-trip time. Amodo Design assumes a 1 ms round-trip time, "expected to be a safe overestimate" ⁵.
• No remote memory. The MIRI system overview says verification depends on ruling out remote memory access, "either via response latency or physical disconnection" ⁴.

Timed challenges are covered in Timed challenge-response and memory-occupation challenges.