# 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: - [x] Panic-surface inventory: audited `panic!`, `assert!`, `unwrap`, and `expect` reachable from manifest, ELF, SQE, params, result-buffer, IPC, and spawn inputs. - [x] 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. - [x] 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`. - [x] Authority graph and resource accounting design for transfer model: `docs/authority-accounting-transfer-design.md`. - [x] 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. - [x] 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. - [x] ELF parser arbitrary-input coverage: proptest coverage plus a bounded `cargo-fuzz` target. - [x] 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`. - [x] 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. - [x] 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. - [x] 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.