Authority Graph and Resource Accounting for Transfer

This document defines the authority graph and resource-accounting contract originally tracked as Security Verification Track S.9 in docs/proposals/security-and-verification-proposal.md. It covers:

• capability transfer (xfer_cap_count, copy/move, rollback)
• ProcessSpawner prerequisites (spawn quotas and result-cap insertion)

The system-wide classification of structural ceilings, quotas, reservations, admission, backpressure, and fairness lives in Resource Governance. This document owns the transaction and exactly-once accounting mechanics used by transfer and spawn; it does not turn capability holds into quantitative entitlements.

Security Verification Track S.9 is complete when this design contract is concrete enough to guide implementation. The invariants and acceptance criteria below are implementation gates for capability transfer, ProcessSpawner, Security Verification Track S.8, and Security Verification Track S.12 follow-up work, not requirements for declaring the Security Verification Track S.9 design artifact complete. Current capability-semantics follow-up items live in docs/backlog/stage-6-capability-semantics.md.

Current Implementation and Target Contract

The current implementation defines ResourceLedger fields in capos-lib/src/cap_table.rs for capability slots, outstanding calls, scratch bytes, frame-grant pages, and virtual-reservation pages. Cap-slot and frame/virtual page reservations are wired into current reservation paths. Outstanding-call and scratch-byte counters are present ledger fields but are not yet fully wired into reservation/preflight paths. Invalid-submission diagnostic rate accounting is implemented by the kernel-global fixed ledger described in §3; it is deliberately not a parallel ResourceLedger counter. Endpoint queue quota, general log-byte accounting, and CPU token-bucket accounting remain target contract fields for future implementation work.

1. Authority Graph Model

Authority is modeled as a directed multigraph:

• Nodes:
  • Process(Pid)
  • Object(ObjectId) (kernel object identity, independent of per-process CapId)
• Edges:
  • Hold(Pid -> ObjectId) with metadata:
    • cap_id (table-local handle)
    • interface_id
    • badge
    • transfer_mode (copy, move, non_transferable)
    • origin (kernel, spawn_grant, ipc_transfer, result_cap)

Security invariant A1: all qualitative object authority is represented by Hold edges; no operation can create object authority outside this graph. Quantitative spend authority is represented separately by a generation-bound resource ledger, reservation token, or delegated grant.

Security invariant A2: each process mutates only its own CapTable edges except through explicit transfer/spawn transactions validated by the kernel.

Security invariant A3: for every live Hold edge there is exactly one cap_id slot in one process table referencing the object generation.

2. Per-Process Resource Ledger and Quantitative Authority

Each process owns a kernel-maintained ResourceLedger. For wired reservation paths, enforcement is fail-closed at reservation time (before side effects). The target contract completes enforcement for present-but-unwired fields and extends the ledger with endpoint queue, general log-byte, and CPU budget counters. The bounded invalid-submission ledger in §3 is a separate kernel-global diagnostic resource with one authoritative accounting record.

ResourceLedger {
  // Current ledger fields.
  cap_slots_used / cap_slots_max
  outstanding_calls_used / outstanding_calls_max
  scratch_bytes_used / scratch_bytes_max
  frame_grant_pages_used / frame_grant_pages_max
  virtual_reservation_pages_used / virtual_reservation_pages_max

  // Target/future fields.
  endpoint_queue_used / endpoint_queue_max
  log_bytes_window_used / log_bytes_per_window (token bucket)
  cpu_time_us_window_used / cpu_budget_us_per_window (token bucket)
}

Current structural and proof values used during Stage 6/5.2 bring-up include:

• cap_slots_max: 256
• outstanding_calls_max: 64
• scratch_bytes_max: 256 KiB
• frame_grant_pages_max: 4096 pages (16 MiB at 4 KiB pages)
• virtual_reservation_pages_max: kernel-configured virtual reservation budget
• Candidate future policy values include endpoint_queue_max 128 messages, log_bytes_per_window 64 KiB/sec with 256 KiB burst, and cpu_budget_us_per_window 10,000 us per 100,000 us window.

These literals do not constitute a production quota profile or minimum-service contract. Cap and thread profile values reach current process construction; frame/virtual maxima remain ledger/ABI values; outstanding-call and scratch reservation paths are incomplete; and endpoint limits are per object rather than aggregate per process. The effective value must eventually be derived from structural capacity, admitted pool credit, delegated parent/subtree credit, and selected policy as defined by Resource Governance.

Security invariant Q1: no counter may exceed its max.

Security invariant Q2: every resource reservation has a typed, generation-bound token and a matched exactly-once release on all success, error, timeout, process-exit, and rollback paths. Double, stale, oversized, and missing releases are detected and audited or recovered; saturating arithmetic must not hide a ledger mismatch.

Security invariant Q3: quota checks for transfer/spawn happen before mutating sender or receiver capability state.

3. Diagnostic Rate Limiting and Aggregation

Repeated invalid ring/cap submissions are aggregated per process and error key.

• Key: (pid, error_code, opcode, cap_id_bucket)
• Buckets:
  • cap_id_bucket = exact cap id for stale/invalid cap failures
  • cap_id_bucket = 0 for structural ring errors
• Per-key token bucket: allow first N=4 emissions/sec, then suppress.
• Per-process output bucket: at most eight detail or summary lines/sec across all of that process’s keys.
• Kernel-global output bucket: at most 16 detail or summary lines/sec.
• Suppressed counts become eligible after one second. Caller-driven ring service attempts at most one due summary before each service, and process teardown emits one final aggregate for any remaining suppressed count:
  • pid=X invalid submissions suppressed=Y last_err=... last_cause=...

kernel/src/cap/ring.rs owns the single ledger of record. It is a kernel-global, statically allocated table with explicit physical budgets of 256 key entries and 256 noisy-process owner records; neither capacity is derived from the per-process capability-slot ABI. Each record is compile-time bounded to 64 bytes, so the two tables reserve at most 32 KiB. Each process may hold at most eight active keys, so one process cannot occupy the shared table. Suppression caused by that share or by key-table pressure is charged to the submitting process’s owner record with its last error and typed capability-error cause; another process’s accounting is not overwritten. Process teardown aggregates pending key and overflow counts into one reason=process-exit summary, removes all of that PID’s keys, and releases its owner slot. PID churn therefore recovers capacity instead of permanently wedging the ledger.

An empty entry admits immediately within the process share. Expired entries are reusable, with pending counts transferred to the evicted entry’s owner record. When a process’s eight entries are all active, new keys are charged to that process’s overflow count without formatting a detail line. This makes key churn observable without allowing first-observation traffic to bypass the per-process or global emission ceilings. A newly admitted key emits its first observation while those physical output budgets have capacity; otherwise its suppression remains attributed to the same process and is summarized later.

Timer-driven ring service records invalid submissions but does not poll the ledger merely to flush summaries. Caller-driven cap_enter and syscall-kicked SQPOLL service attempt one due summary before checking whether the SQ is empty; process teardown handles a burst that stops immediately before exit. Ledger critical sections run with local interrupts disabled, preventing same-CPU interrupt re-entry while preserving the single global ledger.

The emission path allocates no heap memory. It drops the ledger lock before formatting, and serial::write_bounded_diagnostic_line formats through its preallocated 512-byte stack buffer. It tries the UART lock without waiting and uses the bounded lock-free emergency writer if an interrupt preempted the lock owner, so diagnostics cannot deadlock the timer path. Thus an attacker pays for each rejected SQE and bounded fixed-table scans. Detail and ordinary summary lines remain bounded to eight per process and 16 kernel-wide in any one-second window, plus one final process-exit summary. The identity-free invalid-submission-readback observer is outside those emission budgets: it emits on boot and occupancy/high-water changes, and samples counter-only changes at powers of two. One process can cause at most eight key-insertion occupancy records before reaching its active-key share, plus its owner/key teardown record, but process churn can repeat owner occupancy changes without a one-second output charge. Each due observer formats exactly one copied snapshot. The emission guard prevents recursive ownership; a contending caller keeps its snapshot and uses the same non-blocking UART try-lock and bounded emergency fallback instead of waiting, retrying, or dropping the record. Concurrent emergency output may interleave, as it can for other timer-side diagnostics. This readback establishes no UART quota or protected output lane. Application exceptions and ordinary cancellation/pipeline race results remain controlled CQEs and do not enter this invalid-submission ledger. Capability lookup failures retain a typed cause in the key and line rather than collapsing distinct CapError variants into the ring error code.

Security invariant D1: invalid submission floods cannot consume unbounded serial bandwidth or scheduler time in log formatting.

Security invariant D2: one process cannot monopolize the key table or overwrite another process’s overflow attribution. First observations are admitted within the bounded per-process and global output budgets; capacity exhaustion and suppression remain attributable to the submitting process through a bounded summary rather than bypassing D1.

4. Transfer and Rollback Semantics

Transfers (xfer_cap_count > 0) use a kernel transfer transaction (TransferTxn) scoped to a single SQE dispatch. The current ring ABI does not provide kernel-owned SQE sequence numbers or a durable transaction table, so userspace replay of a copy-transfer SQE is repeatable: each replay is treated as a new copy grant. Move-transfer replay fails closed after the source slot is removed or reserved by the first successful dispatch.

Future exactly-once replay suppression requires transaction identity scoped to (sender_pid, call_id, sqe_seq) and a monotonic transfer epoch. Until that exists, exactly-once claims apply only within one dispatch attempt, not across malicious rewrites of shared SQ ring indexes.

Sensitive interfaces must choose their transfer mode deliberately:

Copy-transfer replay is therefore acceptable only for caps whose interface contract says repeated receivers are safe. Sensitive caps must be move-only or non-transferable until the interface has an explicit replay threat model and hostile tests.

Phases:

1. Prepare:
   • validate SQE transport fields and xfer_cap_count
   • validate sender ownership/generation/transferability for each exported cap
   • reserve receiver quota (cap_slots, outstanding_calls, scratch if needed)
   • pin sender entries in txn state (no sender table mutation yet)
2. Commit:
   • insert destination edges exactly once
   • for copy: increment object refcount/export ref
   • for move: remove sender slot only after destination insertion succeeds
   • publish completion/result
3. Finalize:
   • release transient reservations
   • mark txn terminal (committed or aborted)

On any error before Commit, rollback is full:

• receiver inserts are not visible
• sender slots/refcounts unchanged
• reservations released
• CQE returns transfer failure (CAP_ERR_TRANSFER_ABORTED / subtype)

On error during Commit, kernel executes compensating rollback to preserve exactly-once visibility: either all inserts are visible with matching sender state transition, or none are visible.

Security invariant T1: each transfer descriptor is applied at most once within a single SQE dispatch attempt.

Security invariant T2: move transfer is atomic from observer perspective; no state exists where both sender and receiver lose authority due to partial apply.

Security invariant T3: copy-transfer SQE replay is explicitly repeatable until kernel-owned transaction identity exists. Move-transfer replay fails closed after source removal or source reservation.

Security invariant T4: CAP_OP_RELEASE removes one local hold edge only from the caller table and decrements remote export refs exactly once.

5. Integration with 3.6 Capability Transfer

3.6 implementation must consume this design directly:

• CALL and RETURN validate all currently-reserved transfer fields fail-closed when unsupported.
• xfer_cap_count path is wired through TransferTxn (no ad hoc direct inserts).
• Badge propagation is explicit in transfer descriptors and copied into destination edge metadata.
• CAP_OP_RELEASE uses the same authority ledger and refcount bookkeeping.

3.6 acceptance criteria:

1. Copy transfer produces one new receiver edge and retains sender edge.
2. Move transfer produces one new receiver edge and deletes sender edge atomically.
3. Any transfer failure leaves sender and receiver CapTables unchanged.
4. Copy replay is an explicit repeatable-grant policy until a kernel-owned transaction identity is added; move replay fails closed after source removal or reservation.
5. CAP_OP_RELEASE on stale/non-owned cap fails closed without mutating other process tables.

6. Integration with 5.2 ProcessSpawner Prerequisites

5.2 must use the same accounting and transfer machinery:

• spawn() preflights child quotas (cap_slots, outstanding_calls, scratch, frame_grant_pages, endpoint queue baseline) before mapping child memory or scheduling.
• Parent-provided CapGrant entries are inserted via the same transfer transaction semantics (copy for initial grants in 5.2.2).
• Returned ProcessHandle is inserted through the standard result-cap insertion path and accounted as a normal cap slot.
• Child setup rollback must unwind:
  • address space mappings
  • ring page
  • CapSet page
  • kernel stack
  • allocated frames
  • provisional capability edges/reservations

5.2 acceptance criteria:

1. Spawn failure at any step leaves no child-visible process and no leaked ledger usage.
2. Successful spawn accounts all child bootstrap resources within quotas.
3. Parent and child cap-table accounting remains balanced under repeated spawn/exit cycles.
4. ProcessHandle.wait and exit cleanup release outstanding-call/scratch/frame usage deterministically.

7. Implementation Notes for Verification Tracks

This design unblocks:

• Security Verification Track S.8 hostile-input tests for quota and invalid-transfer failures.
• Security Verification Track S.12 Kani bounds refresh for ledger and transfer invariants.
• Target 12 in docs/proposals/security-and-verification-proposal.md with explicit allocator hooks and fail-closed exhaustion behavior.