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

Security And Verification Backlog

Detailed decompositions for security and verification work. Loopyard tasks link here but should not inline these subtasks.

Stage-6 Trust-Boundary Refresh

  • Refresh trust-boundary docs after Stage 6 IPC/capability-transfer work.

Untrusted-Service Hardening Pass

Cover unmapped pointers, kernel-half pointers, invalid capability IDs, corrupted rings, SQ/CQ overflow behavior, and a service without Console authority. Audit manifest, ELF, SQE, params, and result-buffer paths so untrusted input fails closed instead of reaching kernel panic paths.

Completed context:

  • Panic-surface inventory: audited panic!, assert!, unwrap, and expect reachable from manifest, ELF, SQE, params, result-buffer, IPC, and spawn inputs.
  • Ring/user-pointer hostile demos: added unmapped params/result-pointer, kernel-half params-path, invalid-capability-ID, corrupted RETURN call_id, corrupted SQ/CQ head, undersized-params, undersized-result, and SQ/CQ overflow coverage.
  • No-authority smoke: empty-CapSet service verifies expected cap lookups fail and invalid-cap CALLs return controlled CQEs; after removal of syscall 0, it proves a no-authority process cannot write and can only exit/cap_enter.

Remaining decomposition:

  • Quota and exhaustion smokes (make test-untrusted-exhaustion, two QEMU passes; covered 2026-05-25 06:42 EEST):
    • Cap-table and endpoint-queue exhaustion fail closed without corrupting existing calls. Endpoint-queue is proven by the small-scratch core pass (per-owner queue ceiling -> Overloaded, then a held console call still completes). Cap-table is proven by the small-scratch core pass and the default-profile *-captable companion pass: single-frame MemoryObject allocations first return bounded FrameAllocator success replies, then continue until the per-process cap-slot ledger fails closed (Overloaded: failed to reserve MemoryObject cap slot); a held console call still completes after the boundary.
    • Scratch/result-buffer pressure returns controlled errors and later valid calls still complete (core pass: ring-scratch oversize CALL rejected with CAP_ERR_INVALID_REQUEST, reply-scratch clamp returns a serialized exception, then a valid console write completes).
    • Repeated invalid submissions stay bounded: each structurally invalid SQE returns a controlled per-SQE error CQE and the ring stays usable (a recovery NOP completes). The same smoke proves four-line per-key suppression, typed summaries, and wire-valid invalid-cap CAP_OP_RELEASE, CAP_OP_RECV, and CAP_OP_RETURN routing owned by docs/authority-accounting-transfer-design.md §3. The independently higher per-process ceiling makes the four-line single-key assertion sensitive to the per-key bucket. The corrupted-SQ detail count and six userspace-controlled corrupted-CQ recoveries raising the process-exit aggregate from two to eight prove those lifecycle routes. Absence checks for former direct log strings are reintroduction tripwires; the fixed per-process and kernel-global ceilings remain implementation invariants rather than QEMU load claims.
    • Frame-grant-page exhaustion is covered by the cargo test-lib host gate. frame_grant_page_ledger_boundary_is_fail_closed_and_reusable reserves all PROCESS_FRAME_GRANT_PAGE_LIMIT pages, proves the first crossing and an overflowing request leave the complete resource-ledger snapshot unchanged, and proves exact release permits readmission. multi_page_frame_grant_exhaustion_precedes_cap_slot_exhaustion proves one grant larger than the remaining page budget returns the distinct frame-grant error while cap-slot capacity remains available. This is ledger-level fail-closed evidence, not a QEMU smoke or a claim about physical-fragmentation behavior: single-page allocations still reach PROCESS_CAP_SLOT_LIMIT first, while smoke-sized large contiguous allocations can fail from fragmentation before reaching the page ledger.
  • Fail-closed cleanup: the FrameAllocator success-path result serialization now honors the caller’s effective reply-scratch capacity, so small-scratch processes can receive bounded MemoryObject result caps before cap-slot exhaustion fails closed. Closed by security-reply-scratch-success-path-limit-local-proof.

Kani Harness Bounds Refresh

  • make kani-ring – four bounded Kani 0.67.0 harnesses over the pure capos_config::ring core, completed 2026-08-02 15:59 UTC. The gate runs each harness with sqe-validation-oracle alone and with sqe-validation-oracle,measure, so the measure-only PARK_BENCH accept and reject paths are checked. One SQE harness makes every field symbolic at its full fixed width to establish total, panic-free validation. A separate harness symbolically selects the existing independent oracle’s generated valid cases and one-field invalid mutations; it does not mirror the validator’s opcode dispatch or reuse its invalid-shape predicates. Input non-mutation follows from the validator’s shared reference to a plain-integer CapSqe; it is a Rust type-boundary property, not attributed to Kani. The transfer-region harness uses arbitrary u64 address, u32 length, and u16 count values and checks the result against independently composed checked arithmetic. The SQ/CQ harness uses arbitrary u32 head/tail pairs, including wrap, and proves every accepted pending count is within the 16-entry SQ or 32-entry CQ bound; corrupt distances select the producer tail as the recovery head. Concrete accepted/rejected, fit/overflow, and wrap/corruption witnesses keep the checked branches non-vacuous. The eight gate runs completed with 0/3,794 failed Kani checks. These are bounded model checks over fixed-width pure functions, not an unbounded proof of the concurrent ring protocol or kernel dispatcher.
  • Extend Kani coverage from the pure ring core to an explicit bounded ring-protocol publication/ownership state machine, completed 2026-08-02 19:55 UTC. The model uses the ABI’s fixed 16-entry SQ and 32-entry CQ capacities and explores eight symbolic transition attempts per trace. It admits an SQ tail advance only after the selected SQE slot is written, gives at most one Syscall or Sqpoll consumer an exclusive lease over the published head, preserves the SQE value through CQ staging/publication, and admits a ready/wake signal only after CQ-tail publication. Rejected-order witnesses and complete accepted traces for both consumer identities keep those branches non-vacuous. A separate Kani harness invokes the production RingSqConsumerState and checks duplicate-owner exclusion plus stale-generation rejection across Syscall-to-Sqpoll owner turnover. The expanded fourteen default/measure harness configurations completed 2026-08-02 20:41 UTC with 0/7,948 failed Kani checks. The publication model itself shares only the ring-capacity constants with production code and abstracts release/acquire visibility into slot phases: atomic weak-memory interleavings, SQPOLL sleep/wake and teardown races, counter-wrap recovery, and endpoint-promise waiter races remain Loom-only or are covered by the separate pure-core harnesses. The gate is not a proof of the volatile ring page, kernel/src/cap/ring.rs, the scheduler, or the kernel dispatcher.
  • Revisit Kani harness bounds and proof shape once capability transfer, resource accounting, or user-buffer validation has more concrete proof obligations. Keep current bounds practical for make kani-lib; expand only when the added verifier cost buys a specific kernel invariant.

DMA Assurance Model Operationalization

dma-assurance-model-v0 (2026-05-24) landed the accepted proposal (docs/proposals/dma-assurance-model-proposal.md) and inspectable-only TLA+/Alloy skeletons (models/dma/), but stopped there: no run target, no CI gate, no reconciliation with DMA code landed since. Kickoff task: dma-assurance-model-operationalization (decomposition — reconciled the v0 model with landed code and emitted the per-tool slices below).

  • Reconcile models/dma/ with landed invariants (ownership-generation on recycle, map-record-before-PTE-install ordering, drive-pin, epoch fence, scrub-before-free): gap table in models/dma/README.md grounded against the landed symbols, done 2026-06-04.
  • make model-dma-tla — bounded TLC run of dma_authority.tla (pinned TLC 2.19 / tla2tools 1.7.4 + pinned Temurin JRE 17.0.19), lifecycle ordering plus generation-keyed stale completion, record-before-PTE-install split, drive-pin/quarantine, and queue-enable epoch-fence interleavings, checked clean at 2 devices / 2 domains / 2 pages / 2 iovas, generations 0..1, done 2026-06-04: dma-assurance-model-tla-checked-gate.
  • make model-dma-alloy — Alloy analysis of dma_authority.als (pinned Alloy Analyzer 6.2.0), device/domain/IOVA/page/alias authority graph plus the ownership-generation stale-handle gate, checked at scope for 4, done 2026-06-04: dma-assurance-model-alloy-checked-gate.
  • make kani-dma-authority — bounded Kani over an extracted pure DMA-authority core (capos_lib::dma_authority: ownership-generation bump on recycle, stale-handle rejection without mutation, no-re-expose before completion), make kani-lib style, done 2026-06-04. Faithful extraction of the device_dma.rs authority arithmetic; routing the kernel call site through the core is a tracked follow-up (kernel is no_std/no_main, not host-built): dma-assurance-model-kani-authority-core.
  • make model-dma-deferred-completion-loom — focused Loom (pinned 0.7.2) over the DeferredCompletionQueue reservation budget and the multi-CPU TLB shootdown generation re-read (deferred-EOI / completion concurrency the ring Loom does not cover), done 2026-06-04: dma-assurance-model-deferred-completion-loom.
  • Wiring into the Actions workflow and the local aggregate now that each target has a checked result. make dma-assurance-model-check runs Alloy/TLA+/Loom/ Kani locally when cargo-kani is installed and is the enforcing path. The Actions workflow carries the same targets – model-dma-alloy, model-dma-tla, and model-dma-deferred-completion-loom in dma-assurance-models, and kani-dma-authority in kani-proofs – but it fires only on release tags and workflow_dispatch, so it gates nothing before merge. Done 2026-06-05: dma-assurance-model-ci-wiring.

Scheduler & IRQ Assurance Models

The scheduler is the densest unmodeled concurrency surface in the kernel (per-CPU atomics read lock-free from ISR context while another path holds the scheduler mutex via try_lock, plus IPI cross-CPU activation) and has zero formal coverage today (smoke + measured suppressed-tick counters only). The IRQ MSI-X waiter race was fixed by reproduction, not a model. Mirrors the DMA operationalization pattern; tasks reuse the TLC/Alloy/Kani pins that track lands.

  • S1 scheduler-nohz-activation-model (done 2026-06-04 09:00 UTC) – TLA+/TLC for the nohz activation/rollback lifecycle + a focused Loom for the lock-free NOHZ_ACTIVE_CPUS bit vs locked nohz_activation[slot] record race. make model-scheduler-nohz-tla checks no timer-less CPU (NoTimerlessStall + EventuallyReArmed), bit/record agreement (EventuallyConsistent), and that a staled remote activation is dropped not applied to a newer lease (NoStaleActivation + StaledRecordEventuallyCleared); make model-scheduler-nohz-loom checks the lock-free-bit ↔ locked-record reconciliation keeps the timer armed. Checked results + mutation/non-vacuity evidence in models/scheduler/README.md.
  • S2 scheduler-lapic-oneshot-timer-model (done 2026-06-04) – Kani over the extracted pure count/clamp arithmetic (capos_lib::clockevent) + a TLA+ mode-transition lemma pinning the halt-first reprogram ordering. make kani-lapic-oneshot proves the clamp window is well-formed, the armed count is in [1, u32::MAX] with no u128 overflow, and the count round-trips to the request within one LAPIC count (3/3 SUCCESSFUL). make model-scheduler-lapic-oneshot-tla checks that after the halt-first reprogram the next fire is the one-shot at the armed count, never the periodic reload (OneshotModeBoundedCount + HaltedDisarmed + the periodicFiredInOneshotMode sentinel), and that every fire path (user- and kernel-mode consumption) restores a timer source (NoTimerlessStall + EventuallyReArmed / FiredEventuallyRestored liveness). Checked results + mutation/non-vacuity evidence in models/scheduler/README.md.
  • S3/S4 scheduler-cpu-isolation-lease-authority-model (done 2026-06-04 07:04 UTC) – Alloy for the lease/grant relational invariants + TLA+ for the two-lock teardown and the documented non-atomic createLease-vs-revokeGrant SMP window. make model-scheduler-lease-alloy checks the unforgeable grant->lease binding, no live lease through a revoked grant outside the explicitly modeled bounded window, capacity never undercounting a live lease, and the stale-handle generation gate; make model-scheduler-lease-tla checks generation advances exactly once per termination, no capacity double-free, the single chokepoint always runs unregister + SQPOLL-stop + nohz-rollback before recycle, no stranded generation (liveness), and that the renew deadline branch never resurrects. Checked results + non-vacuity evidence in models/scheduler/README.md.
  • IRQ irq-msix-waiter-determinism-model (done 2026-06-04 06:10 UTC) – TLA+/TLC for the waiter <-> delivery <-> deferred-EOI ordering the RX MSI-X waiter fix established. make model-irq-waiter-tla checks no spurious/early injection (NoCompletedEarly), exactly-once delivery/EOI/completion accounting, EOI drain before route re-arm (EpochDrainSound), and the NoLostWake liveness property; checked result + mutation evidence in models/irq/README.md.

Preserved Completed Security Context

These are completed and should not be re-read by default. They remain here so future work can find their design context without bloating loopyard task records.

  • Authority graph and resource accounting design for transfer model: docs/authority-accounting-transfer-design.md.
  • Supply-chain and generated-code TCB hardening: pinned Limine and external build downloads, generated-code drift checks, dependency policy, pinned Cap’n Proto compiler, shared tools/capnp-build, and deterministic generated-binding comparisons.
  • DMA isolation model before PCI/virtio/user-driver work: docs/dma-isolation-design.md defines short-term QEMU bounce-buffer decision, DMAPool, DeviceMmio, Interrupt invariants, and the userspace-driver transition gate.
  • ELF parser arbitrary-input coverage: proptest coverage plus a bounded cargo-fuzz target.
  • Telnet IAC filter fuzz coverage: TelnetFilter extracted to capos-lib::telnet, fuzz/fuzz_targets/telnet_filter.rs exercises the state machine with structural assertions (Normal/AfterIac emission rules, monotonic emit count). Will travel with the parser when networking moves to userspace per docs/proposals/networking-proposal.md.
  • Telnet IAC filter differential round-trip fuzzing (fuzz/fuzz_targets/telnet_filter_roundtrip.rs): synthesize arbitrary RFC 854 event streams (Data, WILL/WONT/DO/DONT, SB blocks with payload), encode to wire bytes, and assert that filter output equals the concatenated Data payloads. Found a real EXOPL handling bug in the original filter – the option byte right after IAC SB was being interpreted as the start of an IAC IAC escape, leaving the filter stuck in the subnegotiation state and silently dropping all subsequent data bytes. Fixed via a new AfterSb state that consumes the option byte unconditionally before entering payload parsing.
  • Line discipline extraction and fuzz coverage: pure LineDiscipline lives in capos-lib::line_discipline, returning LineStep { outcome, echo } descriptions. The kernel transport drives it and translates Echo::Byte/Echo::Backspace/Cancelled/ Submitted/Reprompt into the existing send_*_track_cr calls. Backed by fuzz/fuzz_targets/line_discipline.rs with structural invariants (line_len <= max_bytes, ±1 line_len delta per Pending step, Cancelled clears, echo only when buffer grows/shrinks).
  • Future: differential fuzzing against an external Telnet library (libtelnet or a Rust port) to catch RFC conformance bugs the structural and round-trip targets cannot express. Tracked as a follow-up to the Telnet IAC filter fuzz coverage track (S.14).
  • Ring SQE wire validation extraction and fuzz coverage: lifted the per-opcode *_sqe_has_unsupported_fields predicates from the kernel into capos_config::ring, exposed a unified sqe_wire_validation_error entry point, and reroute the kernel through it. Added fuzz/fuzz_targets/sqe_validation.rs plus 12 host unit tests covering the classification boundaries each opcode imposes. Closes the originally planned three-parser fuzz set (elf::parse, manifest::decode, ring SQE decoder).
  • Well-formed SQE generator oracle (security-sqe-well-formed-generator-fuzz-local-proof): the test/fuzz-only sqe-validation-oracle feature exposes capos_config::ring::sqe_oracle, which generates validator-accepted SQEs for every opcode accepted by the current build, plus one-field rejecting mutations for reserved fields, unsupported flags, constrained cap/pointer/size fields, opcode-specific constraints, and session-disclosure reserved bits. The existing sqe_validation fuzz target keeps arbitrary-byte coverage and runs the positive/negative oracle on each input. This closes the shared wire-validator oracle gap only; it does not claim cap-table lookup, userspace pointer mapping, transfer-descriptor loading, or full kernel ring semantic coverage.
  • Track S.17 – sanitizers on host tests – partially landed. make sanitizer-host-tests runs AddressSanitizer over the capos-lib and capos-config host suites (crate set / features mirror the test-lib / test-config aliases). Outcome: zero findings – both suites pass clean under ASan, including the named unsafe suspects (FrameBitmap slot indexing, CapTable generation counters, lazy_buffer raw &mut [u8]). The “cheap to add” claim holds for ASan only: it needs no -Zbuild-std because its libc interceptors cover the uninstrumented precompiled std. - ThreadSanitizer (make sanitizer-host-tests-tsan) is blocked upstream, not by a capOS defect. TSan changes the crate ABI, so rustc refuses to link sanitized code against the uninstrumented precompiled std (mixing -Zsanitizer will cause an ABI mismatch). Instrumenting std needs -Zbuild-std, which then fails with duplicate lang item in crate core: sized for build-script-bearing dependencies (typenum / libc / cfg-if / subtle) when the sanitizer target equals the host triple – reproduced four ways (plain -Zbuild-std, renamed --target JSON spec, target-applies-to-host=false, and -Zhost-config). The TSan target is kept wired so it starts passing once the upstream -Zbuild-std + build-script issue is fixed. capOS concurrency invariants are meanwhile covered by the dedicated Loom model (cargo test-ring-loom); these host unit tests spawn no threads, so TSan’s marginal value here is low.