Keyboard shortcuts

Press ← or → to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

Whitepaper Evidence Gaps

Live tracking of which paper claims still lack artifact-level evidence and which workplan slice will close each gap. Update this file in the same task that closes a gap. When a gap closes, also update the corresponding #todo block in the paper draft at papers/schema-as-abi/main.typ.

Claim C1: Schema-typed methods replace parallel rights

Status: partial.

  • Capability dispatch via CapObject + capnp schema (kernel + capos-rt).
  • Authority narrowing via wrapper capabilities (no rights bitmask).
  • Stage 6 Gate 0: delegated endpoint relabeling containment.
  • Transitional service-object representation and selector preservation substrate for endpoint-backed service facets.
  • Historical service-object routing/lifecycle proof: synthetic receiver-cookie spoofing, lifecycle, and transfer coverage in commit a4655f0.
  • Session-Bound Invocation Context Gate 1: one immutable session context per process, with child inheritance and hostile second-session injection checks, demonstrated by make run-session-context.
  • Session-Bound Invocation Context Gate 2: privacy-preserving endpoint caller-session metadata, explicit subject disclosure, and payload spoofing/disclosure hostile checks.
  • Session-Bound Invocation Context Gate 3: chat / adventure / stdio migrated off caller-selected endpoint identity to session-keyed service authority.
  • Trust-boundary doc refresh recording the post-migration state.

Closes via: docs/backlog/session-bound-invocation-context.md. Already next on the mainline path per WORKPLAN.md.

Claim C2: Ring + one progress syscall is a sufficient boundary

Status: implementation done, numbers missing.

  • cap_enter semantics, SQ/CQ ring, CALL/RECV/RETURN/RELEASE/NOP.
  • Direct-switch IPC handoff.
  • Loom protocol model.
  • make run-measure benchmark-only feature scaffolding.
  • Reproducible measurement run that records:
    • cap_enter warm/cold round-trip latency
    • SQE dispatch throughput
    • Endpoint IPC: scheduler vs. direct-switch handoff latency
    • Schema dispatch overhead vs. NullCap baseline
    • Memory cost per capability slot
  • Tracked path for measurement output so the paper can cite a commit.
  • Optional: comparison numbers from published seL4/Zircon literature where the comparison is fair.

Closes via: a dedicated measurement-harness slice. Not yet in WORKPLAN.md; promote when scheduling allows.

Claim C3: Wire format enables persistence

Status: missing.

  • Minimal RAM-backed Store capability.
  • One non-trivial capability whose state is serialized via its capnp schema, dumped, and restored across kernel reboot in QEMU.
  • Method call on the restored capability returns the expected result.
  • QEMU smoke target wired to this proof.
  • Documentation explicitly scoping this to “paper evidence” rather than the full storage proposal in docs/proposals/storage-and-naming-proposal.md.

Closes via: a paper-scoped persistence-PoC slice, narrower than the storage proposal. Not in WORKPLAN.md yet.

Claim C4: Wire format enables network transparency

Status: missing.

  • RemoteCap shim forwarding one capnp method call over an established TCP capability.
  • Working setup: two capOS QEMU guests, or one capOS guest plus a host capnp stub.
  • QEMU smoke target proving end-to-end success and clean teardown.
  • Documentation explicitly scoping this to “paper evidence” rather than a general network-transparency subsystem.

Closes via: a paper-scoped network-transparency-PoC slice. Naturally rides on the SSH/Telnet networking work in docs/backlog/runtime-network-shell.md.

Claim C5: Practical kernel verification at this size

Status: strong, needs distillation.

  • Bounded Kani gates: cap-table, frame-bitmap, transfer rollback, resource accounting.
  • Loom ring model.
  • Miri host-test path.
  • Panic-surface inventory.
  • Dependency policy (cargo-deny, cargo-audit).
  • Trusted build inputs inventory.
  • Ring protocol Kani proof (currently Loom-only) – Tier-2 strengthener.
  • Concise summary table for the paper: invariant, tool, scope, bounds.

Closes via: docs/backlog/security-verification.md plus a paper-section distillation pass.

Cross-cutting strengtheners

Not blocking the thesis, but materially raise quality:

  • SSH Shell Gateway end-to-end. Paused behind the selected Session-Bound Invocation Context milestone, but still the concrete external-facing artifact for §6 when remote shell work resumes.
  • Full concurrent SMP scheduling. Removes a single-CPU asterisk.
  • One non-toy demo beyond Adventure / First Chat: storage-backed or federated, depending on which composes with C3 / C4.

How to update this file

Update in the same task that lands the artifact. When ticking a checkbox:

  1. Reference the closing commit or branch.
  2. If the closing artifact reframes the claim, update plan.md and outline.md in the same task.
  3. If a Tier-1 gap closes, revisit WORKPLAN.md to verify paper-driven sequencing still matches the next mainline slice.