Security And Verification Backlog

Detailed decompositions for security and verification work. WORKPLAN.md links 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:
  • Cap-table and endpoint-queue exhaustion fail closed without corrupting existing calls.
  • Scratch/result-buffer pressure returns controlled errors and later valid calls still complete.
  • Repeated invalid submissions are rate-limited or aggregated according to authority-accounting policy.
  • Frame exhaustion boundary is covered once the relevant ledger is reachable from a smoke.
• Fail-closed cleanup: replace remaining trust-boundary panics with controlled CQE/application errors or an explicitly documented kernel halt policy.

Kani Harness Bounds Refresh

• 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.

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 WORKPLAN.md.

• 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 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).
• Future: paired with the SQE validation work, a randomised “well-formed SQE generator” target would give the fuzzer an oracle to disagree with – generate valid SQEs for each opcode and assert acceptance, then mutate single fields and assert rejection. Today’s sqe_validation target only pins behavior.
• Future: sanitizers on host tests (RUSTFLAGS=-Zsanitizer=address and thread) wired into cargo test-lib (and the other host-test aliases) under nightly as a CI job. Design source: §Tier 2 of docs/proposals/security-and-verification-proposal.md. Tracked as Track S.17. The proposal’s claim that this is “cheap to add” should be validated by actually adding it – expect to discover whether unsafe blocks in capos-lib / capos-config flag any latent UB or data-race patterns once they are exercised under sanitizers.