# DMA Assurance Model

Current DMA authority and isolation design authority lives in
[`docs/dma-isolation-design.md`](../dma-isolation-design.md). This proposal
defines the accepted evidence model and is retained as the grounding record for
DMA proof obligations.

The DMA assurance model is the evidence scaffold for moving capOS from bounded
QEMU-local provider proofs toward cloud and production device-driver claims. It
does not select a cloud DMA backend. It defines the claims that a backend must
prove, the model objects those claims refer to, and the tools that should check
each claim before a driver slice can cite it.

The immediate use is the cloud DMA backend decision: direct DMA through a
reviewed remapping domain, labeled bounce buffers, or unsupported. The binding
choice and any per-VM-shape safety claim remain attended decisions.

## Claim Boundary

The model is about DMA authority, not whole-kernel correctness.

In scope:

- ownership of `Device`, `DMAPool`, `DMABuffer`, `Page`, `IommuDomain`,
  `Iova`, descriptor, completion, and interrupt-route state;
- lifecycle transitions from allocation through mapping, publication,
  completion, revocation, invalidation, scrub, and reuse;
- stale handle, stale completion, revoke/reset race, teardown-under-DMA,
  no-host-physical-exposure, and cross-domain aliasing claims;
- the evidence split between IOMMU-backed direct DMA and labeled
  bounce-buffer fallback.

Out of scope:

- proving all kernel behavior;
- proving cloud-provider hardware facts without attended evidence;
- treating QEMU Intel VT-d evidence as general hardware evidence;
- creating a new prover or proof kernel.

The capOS-specific layer may become a DSL later, but it must emit to mature
checkers or proof assistants. A self-authenticating capOS prover would increase
the trusted base and is not part of this plan.

## Model Objects

The abstract model uses these terms consistently across docs, model files, and
future proof harnesses:

| Object | Meaning |
| --- | --- |
| `Device` | PCI function or provider device that can issue DMA. |
| `IommuDomain` | Device-manager-owned translation context or trusted sharing group. |
| `DMAPool` | Capability-scoped allocation authority for DMA buffers. |
| `DMABuffer` | Live buffer handle with owner, slot, generation, and mapping state. |
| `Page` | Physical backing page owned by the device manager or held fail-closed. |
| `Iova` | Device-visible address meaningful only inside one domain. |
| `Descriptor` | Device-visible command referencing a live buffer generation. |
| `Completion` | Device or software observation that a descriptor finished. |
| `IrqRoute` | Interrupt source, route generation, waiter, mask, and ack state. |

The first model files live under [`models/dma/`](../../models/dma/). They are
small by design: reviewers should be able to read the whole state machine and
tell whether it matches the DMA design before any checker is involved.

## Required Invariants

| Invariant | Required meaning |
| --- | --- |
| No host-physical exposure | Result caps, diagnostics, audit, and cloud evidence never expose a host physical address to a driver. IOMMU-backed paths may expose only a domain-scoped IOVA labeled with its domain. |
| Mapping before publication | A descriptor cannot become device-visible until the backing buffer is live, owned by the device manager, and either mapped in the selected IOMMU domain or copied through the selected bounce-buffer path. |
| No page reuse before teardown | A DMA page cannot return to the general free pool until submissions are stopped, in-flight descriptors are drained or invalidated, mappings are removed, required invalidations complete, and the page is scrubbed. |
| Stale handles fail closed | A stale pool, buffer, slot, page, source, route, or generation cannot create a new side effect. |
| Stale completions fail closed | A completion whose descriptor, buffer, slot, page, owner, or generation no longer matches cannot publish CQ state, ack IRQ state, free pages, or reuse buffers. |
| Domain-scoped aliasing only | The same IOVA may be reused in different domains, but one domain cannot map the same IOVA to two pages unless an explicit trusted sharing group model permits it. |
| Fail-closed leaks are bounded | If teardown cannot prove that hardware can no longer reach a page, the page or pool may be held, but that hold must be accounted, bounded, and surfaced as a remediation item. |
| Backend evidence is explicit | Direct DMA requires remapping-domain evidence. Bounce-buffer fallback must stay labeled as not hostile-hardware isolation. Unsupported devices stay disabled. |

## Tool Mapping

The assurance model intentionally uses several narrow tools instead of one
large proof.

| Tool | capOS use |
| --- | --- |
| TLA+ / TLC | Model lifecycle ordering and races: allocate, map, publish, complete, revoke, flush, scrub, reuse, reset, and fail-closed hold. The v0 skeleton is [`models/dma/dma_authority.tla`](../../models/dma/dma_authority.tla). |
| Alloy | Model the relational authority graph: device, domain, IOVA, page, owner, and alias constraints. The v0 skeleton is [`models/dma/dma_authority.als`](../../models/dma/dma_authority.als). |
| Kani | Prove pure Rust validators and accounting helpers once they are extracted into host-checkable code: generation matching, budget arithmetic, stale rejection, and fail-closed transitions. |
| Loom | Cover concurrency-sensitive state that depends on atomics, queues, or multi-CPU ordering. The first target was the `DeferredCompletionQueue` / TLB-shootdown model gap now recorded in `docs/tasks/done/2026-06-04/dma-assurance-model-deferred-completion-loom.md`. |
| Verus | Candidate later tool for small critical Rust cores that need unbounded functional contracts and are stable enough to justify annotation cost. |
| HAMR / Microkit | Reference architecture for static component contracts and traceability, not a replacement runtime for capOS. Useful for comparing device-manager and driver partitioning assumptions. |

Do not claim a checked model result merely because the files exist. A checked
claim requires recording the exact tool, version, configuration, model bounds,
and command output in the task evidence.

## V0 Gate

`dma-assurance-model-v0` is complete when:

- this proposal defines the model objects, invariants, tool mapping, and
  claim boundaries;
- `models/dma/` contains inspectable TLA+ and Alloy skeletons for the lifecycle
  and authority graph;
- the cloud DMA backend draft task depends on this model before it can be
  promoted beyond proposal text;
- the verification workflow names these model files as planned design evidence,
  while making clear that no required checker gate exists yet;
- docs workflow and diff hygiene pass.

Future slices should add actual checker commands only after the repo has pinned
tool installation and run targets. Suggested future targets are
`make model-dma-tla`, `make model-dma-alloy`, `make kani-dma-authority`, and a
focused Loom target for `DeferredCompletionQueue`.

## V1 Operationalization

`dma-assurance-model-operationalization` (2026-06-04) reconciles the v0
skeletons with the DMA authority code that landed after them and emits the
checker tracks as concrete task records, so the work cannot be silently parked
again. The reconciliation gap table — which invariants the skeletons already
capture and which landed-since invariants are MISSING — is recorded in
[`models/dma/README.md`](../../models/dma/README.md) and grounded against named
symbols in `kernel/src/device_dma.rs`, `kernel/src/cap/dma_buffer.rs`,
`kernel/src/device_manager/stub.rs`,
`kernel/src/cap/virtio_net_userspace_rx_dma_proof.rs`, and
`kernel/src/arch/x86_64/tlb.rs`.

Landed-since invariants MISSING from the v0 skeletons: ownership-generation bump
on recycle, map-record-before-PTE-install ordering, drive-pin/quarantine, the
queue-enable epoch fence, and the deferred-EOI / completion-queue concurrency.
Each is owned by an emitted checker slice (each names its `make` target, pinned
tool + version, model bounds, and the exact invariant it checks, and each must
record checked output per the anti-overclaim rule above):

| Track | `make` target | Tool | Slice |
| --- | --- | --- | --- |
| Lifecycle ordering + generation + stale-completion | `make model-dma-tla` | TLA+/TLC (pinned; TLC-pin owner shared with the scheduler/IRQ model tracks) | [`dma-assurance-model-tla-checked-gate`](../tasks/done/2026-06-04/dma-assurance-model-tla-checked-gate.md) (**done** 2026-06-04, checked clean at 2/2/2/2, gen 0..1) |
| Device/domain/IOVA/page/alias authority graph + generation | `make model-dma-alloy` | Alloy (pinned 6.2.0; Alloy-pin owner) | [`dma-assurance-model-alloy-checked-gate`](../tasks/done/2026-06-04/dma-assurance-model-alloy-checked-gate.md) (**done** 2026-06-04, checked `for 4`) |
| Extracted pure ownership-generation / stale-handle / no-re-expose core | `make kani-dma-authority` | Kani (pinned 0.67.0, `kani-lib` style) | [`dma-assurance-model-kani-authority-core`](../tasks/done/2026-06-04/dma-assurance-model-kani-authority-core.md) (**done** 2026-06-04, 3 harnesses checked over `capos_lib::dma_authority`) |
| Deferred-EOI / completion-queue concurrency | new Loom target | Loom (`test-ring-loom` sibling) | [`dma-assurance-model-deferred-completion-loom`](../tasks/done/2026-06-04/dma-assurance-model-deferred-completion-loom.md) |
| CI wiring (`make check` / GitHub gate) + cite checked evidence | (wiring only) | — | [`dma-assurance-model-ci-wiring`](../tasks/done/2026-06-05/dma-assurance-model-ci-wiring.md) (**done** 2026-06-05) |

## Cloud Backend Use

The cloud backend draft must cite this model and fill an evidence matrix for
each backend candidate:

| Candidate | Required evidence before sign-off |
| --- | --- |
| Direct remapping domain | Cloud VM shape exposes guest-programmable remapping hardware; capOS can discover and program it; descriptor publication is ordered after mapping; teardown removes mappings and observes required invalidations before page reuse; hostile stale-DMA and stale-completion smokes cover the selected path. |
| Labeled bounce-buffer fallback | Direct DMA remains blocked; all device-visible addresses are manager-owned bounce pages; no host physical address is exposed; stale handle/completion/teardown evidence covers the selected fallback; documentation states that hostile bus-mastering hardware isolation is not claimed. |
| Unsupported | Device remains disabled or unbound; no driver-visible DMA, MMIO doorbell, interrupt ownership, or storage/network readiness claim is made. |

The matrix must distinguish provider-side isolation facts from guest-controlled
isolation facts. SR-IOV, virtual NIC, GPU, accelerator, or local NVMe support is
evidence that a VM exposes DMA-capable device surfaces, but it is not direct
remapping evidence unless the guest also exposes an IOMMU or equivalent
translation authority that capOS can program. Each VM-shape row should record
the provider, region or zone, instance type, image and kernel, provider API or
documentation source and date, live guest probe output, visible PCI/device
drivers, visible IOMMU tables or groups, maintenance/revocation behavior, and
the resulting backend classification.

The matrix is a support-policy input, not a hardcoded boot oracle. capOS should
infer the safest available backend at runtime from the device inventory,
remapping authority it can actually program, driver self-tests, and fail-closed
probe results. Unknown or contradictory observations select `Unsupported`, not
direct DMA. Provider evidence remains necessary for VM shapes the project wants
to advertise as supported, because a guest probe cannot fully prove host-side
provider isolation or maintenance behavior.

The matrix is an input to attended sign-off. It is not itself the sign-off.

## Design Grounding

- [`docs/dma-isolation-design.md`](../dma-isolation-design.md)
- [`docs/research/iommu-remapping.md`](../research/iommu-remapping.md)
- [`docs/research/sel4.md`](../research/sel4.md)
- [`docs/research/sel4-hamr.md`](../research/sel4-hamr.md)
- [`docs/tasks/done/2026-05-23/ddf-iommu-remapping-production-closeout.md`](../tasks/done/2026-05-23/ddf-iommu-remapping-production-closeout.md)
- [`docs/tasks/done/2026-05-23/ddf-provider-virtio-net-driver-closeout.md`](../tasks/done/2026-05-23/ddf-provider-virtio-net-driver-closeout.md)
- TLA+ TLC model checker documentation:
  <https://docs.tlapl.us/using%3Atlc%3Astart>
- Alloy analyzer documentation:
  <https://alloytools.org/faq/what_kind_of_analysis_does_the_alloy_analyzer_do.html>
- Kani Rust verifier documentation:
  <https://model-checking.github.io/kani/>
- Loom crate documentation:
  <https://docs.rs/loom/latest/loom/>
- Verus guide:
  <https://verus-lang.github.io/verus/guide/>