Skip to main content
How Can We Help?
< All Topics
Print

Failure Atomicity in Guest Memory Access: Preflight the Whole Span

Posted
Updated
ByJstar269

Status: IMPLEMENTATION FACT / DERIVED · Evidence: current public runtime source and synthetic negative-path reasoning · Last reviewed: 2026-08-11

The correctness property

Checking only the first guest address is not a proof that a bulk host access is safe. A read or write must validate the complete guest-visible span, including checked size arithmetic, before the host operation begins. When the PSP-visible contract rejects an invalid span, the rejection should happen before partial host or guest side effects.

Preflight model

  1. Validate the requested width and reject impossible or negative sizes.
  2. Compute the inclusive end with overflow-checked arithmetic.
  3. Validate the entire readable or writable span against the guest-memory map.
  4. Only then perform the host copy or decode.
if (!sr_guest_span_readable(addr, size)) return error;
// no host access before the complete span check
copy_from_guest(dst, addr, size);

The same rule applies to writes, pointer-plus-length structures, string buffers with explicit limits, and vector or matrix operations whose lanes cross a page boundary. A start-address check followed by an unchecked addr + size can wrap and turn an invalid request into a host out-of-bounds access.

Current public implementation

The guest-span validators and CpuState ABI expose width-safe span checks and the load-bearing register layout. They are implementation facts that can be reviewed without private EBOOT data. The validation rule also protects the load-bearing CpuState layout: invalid guest pointers must not partially mutate registers, memory, or branch bookkeeping before the error is returned.

Evidence and tests

A useful regression uses a synthetic guest map with a valid first byte and an invalid final byte, then asserts both the return code and the absence of partial side effects. That is a production-helper/white-box or model test unless it reaches a registered PSP NID through the real dispatch path; label it honestly under the Evidence Standard. Add separate cases for integer overflow, zero length, cross-page writes, and failed output buffers.

Failure atomicity is a design contract, not a loop cap or a forced success. It belongs beside the Static Recompilation Architecture, the PSP Executable Model, and the Open Research Questions.

Table of Contents