Writing a partition manifest

The manifest sits in the hypervisor’s own read-only data, covered by no enabled stage-2 region. That is not a separate protection mechanism: ZoneX’s own memory is protected precisely by not being covered by any enabled region, so a guest cannot read the manifest for exactly the same reason it cannot read the hypervisor’s code.

This is stated outright because "the manifest is unreachable from a guest" is a property a reviewer should not have to derive.

A region is a base address, a limit and a set of attributes. The limit is the last byte, inclusive, not one past the end — this matches how the hardware describes a region, and mixing the two conventions is the mistake the validator’s alignment rules exist to catch. Base and limit must both be granule-aligned.

A partition carries an identifier, a name, the range of the guest image embedded in the hypervisor’s own image, the address it starts executing at, its list of regions, and its window in the major frame expressed in ticks.

A shared range is one granule with a single nominated publisher. The publisher may write it; every other partition may only read it.

The manifest is the list of partitions, the list of shared ranges, and the major frame length in ticks.

The manifest states the major frame length explicitly, even though it is the sum of the partition windows.

That is deliberate. A computed field could never disagree with its parts, and therefore could never be wrong — so a frame length that does not match the sum of its windows would be undetectable. Carrying it explicitly lets the validator disagree with it, which turns a class of configuration error into a boot-time diagnosis.

No partition in the Phase-0 demonstrator is granted a device region of any kind. There is one console, and a guest reaches it by asking the hypervisor rather than by being given the peripheral. That is why the temporal figures on the claim page describe two partitions that share nothing but a core.

Granting a partition a device is a later phase, and on this part it carries a constraint worth knowing in advance: peripheral privilege for accesses from this core cannot rest on the memory-domain access controllers, so partition-level device isolation has to be carried by the stage-2 memory protection unit and its region attributes.

A partition is isolated from another by which regions are enabled while it runs, never by permission bits.

This matters when reading the attribute encodings: at stage 2 there is no encoding that grants a guest access while denying EL2. So a region that grants a partition access must be disabled while any other partition runs, and a partition switch is one write that changes the whole enabled set. See the switch-mask budget for the constraint that follows.

One error code per rule, and no code shared between two rules. That is what makes a failure a diagnosis rather than a hint: "the manifest is invalid" sends a reader back to the whole manifest, while an unaligned-limit code carrying a partition index and a region index sends them to the line.

The rules fall into groups.

Shape. A non-null manifest with at least one partition and no more than the build-time maximum; no duplicate partition identifiers; at least one region per partition and no more than the maximum; a non-empty image range that fits the region it is loaded into.

Geometry. Every base and every limit granule-aligned; no limit below its base; no partition’s regions overlapping each other; no partition’s region overlapping another partition’s; no region overlapping the hypervisor’s own device memory.

Attributes. Every access-permission, execute-never and shareability field a legal encoding; every attribute index in range; and every attribute field actually written, so that a partly initialised descriptor is refused rather than programmed.

Executability. Every partition must have at least one executable region and at least one writable region, and its entry point must lie inside one of its own executable regions. A four-byte error in an entry point cost a silicon run during earlier port work, which is why this is a rule rather than an assumption.

Time. No zero-length window, and the major frame must equal the sum of the windows.

Sharing. No more shared ranges than the maximum; each exactly one granule; each with a valid publisher; and access permissions consistent with one writer and any number of readers.

Budget. The planned layout must fit the part’s region count and its switch mask, and every region assigned must have a switch-mask enable bit.

The overlap rule is unconditional and is the one the memory claim rests on: every byte outside a declared shared range is governed by it, with no exceptions.

A real system’s manifest is a constant. The demonstrator images in the repository build theirs at run time from linker symbols instead, because a harness must not restate addresses the linker chose — but that is the harness’s shape, not the product’s, so what follows is the constant form.

Two partitions, a code and a data region each, seven ticks of every ten against three, and no shared range:

Three things about it are worth more than the syntax.

Every field is named. Positional initialisers compile and a dropped field then reads as zero — which for an attribute index means index 0, a memory type that happens to be correct here and would not be in general. Naming the fields makes a missing one a compiler diagnostic.

Both regions are granule-aligned at both ends, and the limit is the LAST byte: 0x3179FFFF, not 0x317A0000. ZX_MPU_GRANULE is the alignment every base and limit is checked against.

The manifest needs no port header. zx_api.h and zx_manifest.h are enough to declare a whole system, which is what lets the host-side validator check the same objects with no target header in reach.

Moving partition B’s code region — and its entry point with it, so that the entry rule does not fire first — onto partition A’s data:

which is ZX_MANIFEST_PARTITION_OVERLAP, and it names both offenders: A’s data region and B’s code region, each by partition and index. An overlap has two parties and a diagnosis that named only one would send a reader to look at the innocent half.

Setting the major frame to eleven ticks while the windows still sum to ten gives 0x18, ZX_MANIFEST_FRAME_MISMATCH, and that one carries no indices at all — the fault belongs to the frame rather than to any partition, and reporting a partition would be inventing a culprit.

For the run-time form built from linker symbols, and for the negative builds that prove each rule can reject, see examples/common/ in the repository.

A shared range is a deliberate hole in total disjointness, and it is worth being honest about its consequence.

It does not weaken the claim that a partition cannot reach another partition’s private memory: every byte outside a declared range is still governed by the unconditional overlap rule. It does mean the two partitions are not information-theoretically isolated — the publisher can signal the reader at one granule’s bandwidth, and a reader cannot be prevented from timing those writes.

A system that needs no covert channel at all declares no shared ranges, and the validator then enforces total disjointness with no exceptions.