Security Review and Formal Verification Proposal

How to reason about the correctness and security of the capOS kernel and its trust boundaries in a way that fits a research OS – pragmatic tooling now, targeted verification where it pays off, no aspirational seL4-style full- kernel proofs. The docs/research/sel4.md survey already concluded that Isabelle/HOL-over-C verification does not transfer to Rust and that the design constraints matter more than the proof artefact. This proposal codifies that conclusion into a concrete tooling and process plan.

This proposal uses CWE for concrete vulnerability classes, CAPEC for attacker patterns, Rust language rules / unsafe-code guidance for low-level coding rules, Common Criteria protection-profile concepts for OS security functions, and capability-kernel practice (seL4/EROS-style invariants) for authority, IPC, object lifetime, and scheduler properties. Web-application checklists are not the baseline for OS design review.

Grounding sources:

• MITRE CWE for root-cause weakness labels: CWE-20 explicitly covers raw data, metadata, sizes, indexes, offsets, syntax, type, consistency, and domain rules; CWE also marks broad classes such as CWE-20 and CWE-400 as discouraged for final vulnerability mapping when a more precise child fits.
• MITRE CAPEC for attacker behavior, especially input manipulation (CAPEC-153), command injection (CAPEC-248), race exploitation (CAPEC-26 / CAPEC-29), and flooding/resource pressure (CAPEC-125).
• Rust Reference and Rust 2024 Edition Guide for unsafe-block and unsafe_op_in_unsafe_fn obligations.
• seL4 MCS and the existing capOS research notes for capability-authorized access to kernel objects and CPU time.
• Common Criteria General Purpose Operating System Protection Profile for OS access-control, security-function, trusted-channel/path, and user-data protection concepts. capOS is not trying to certify against it; the PP is a vocabulary check for what an OS security review should not omit.

1. Philosophy and Scope

capOS is explicitly a research OS whose design principle is “schema-first typed capabilities, minimal kernel, reuse the Rust ecosystem.” Three consequences shape this proposal:

1. The schema is part of the TCB. A bug in the .capnp schema, or in the way generated code is patched for no_std, is exactly as dangerous as a bug in the kernel. The schema, the capnpc build pipeline, and the generated code all need review attention – not only hand-written kernel code.
2. The kernel should stay small. “Everything else is a capability” means the TCB is naturally bounded. Verification effort scales with TCB size, so resisting kernel bloat is itself a security property.
3. The interface is the permission. Access control lives in capnp method definitions and in userspace cap wrappers (a narrow cap is a different CapObject), not in kernel rights bitmasks. Review must confirm that the kernel never short-circuits this: no ambient authority, no method that bypasses CapObject::call, no syscall that exposes an object without a capability handle.

Non-goals:

• Full functional-correctness proof of the kernel à la seL4. Infeasible in Rust today, and the payoff is low for a research system whose surface area is still changing.
• Proving information-flow / confidentiality properties end-to-end.
• Certifying a specific configuration for external deployment.

2. Trust Boundaries and Threat Model

Enumerating the boundaries forces every future review to ask “which boundary does this change touch?” and picks out the code paths that matter.

Current boundaries

Attacker model

• Untrusted service binaries. Today’s services are checked into the repo, but the manifest pipeline is meant to load arbitrary binaries eventually. Assume every byte of a service’s SQEs, params buffers, result buffer pointers, and return addresses is attacker-controlled.
• Untrusted manifest. Once manifests are produced outside the repo (e.g. generated from CUE fragments, passed in as a Limine module), the manifest parser must reject every malformed input without panicking.
• Resource exhaustion. Once multiple mutually-untrusting services run, a service can attack by filling rings, endpoint queues, capability tables, frame pools, scratch arenas, logs, or CPU time. Boundedness and accounting are security properties, not performance polish.
• Build input drift. The schema/codegen path is already part of the TCB. External build inputs such as the bootloader checkout, Rust dependencies, capnp code generation, and generated-code patching must be reproducible enough that review can tell what changed.
• Host tooling input. Build tools and generators run with developer/CI filesystem access. Treat manifest/config-derived paths and command arguments as untrusted until bounded to the intended directory and execution context.
• Residual state and disclosure. Kernel logs, returned buffers, recycled frames, endpoint scratch space, and generated artifacts must not expose kernel pointers, stale bytes from another process, secrets, or build-system paths that increase attacker leverage.
• Hostile interrupts / preemption. The scheduler preempts at arbitrary points. Any kernel invariant that is only transiently true must be held under the right lock or with interrupts disabled.
• Out of scope (for now): physical attacks, speculative-execution side channels, malicious hardware, IOMMU bypass from DMA devices. These become in-scope once the driver stack lands; revisit the threat model then.

3. Tiered Approach

Four tiers, cheapest first. Each tier is independently useful, and later tiers assume earlier ones are in place.

Tier 1 – Hygiene and CI (cheap, high value)

These are the controls that make every other tier work. The initial GitHub Actions baseline exists in .github/workflows/ci.yml; it runs formatting, host tests, cargo build --features qemu, make capos-rt-check, and make generated-code-check. The QEMU smoke job installs its own boot tools and runs make plus make run, but remains non-blocking, so it is not yet a required boot assertion.

• Continuous integration via GitHub Actions (or equivalent). Current baseline: make fmt-check, cargo test-config, cargo test-ring-loom, cargo test-lib, cargo test-mkmanifest, cargo build --features qemu, make capos-rt-check, and make generated-code-check. Remaining CI work: treat QEMU boot as a required CI gate once runtime flakiness is acceptable, then add the security policy jobs below.
• cargo clippy --all-targets -- -D warnings across workspace members, with a curated set of clippy::pedantic / clippy::nursery lints that pay off for kernel code (clippy::undocumented_unsafe_blocks, clippy::missing_safety_doc, clippy::cast_possible_truncation, etc.). Do NOT enable all of pedantic blindly – review each lint and either enable it or add a rationale comment.
• cargo-deny for license and advisory gating; cargo-audit for the RustSec advisory DB against Cargo.lock. Dependencies include capnp, spin, x86_64, limine, linked_list_allocator – all externally maintained.
• cargo-geiger report of unsafe surface area per crate, checked in as a snapshot and diffed in CI so growth is visible in PRs.
• Deny unsafe_op_in_unsafe_fn (already required by edition 2024; make sure it stays on) and missing_docs on public kernel items where it is not already the case.
• Dependency review discipline: every new dep needs a one-line rationale in the commit message and a check that it is no_std-capable, maintained, and does not pull in a surprise async runtime or heavy transitive graph.
• No-std dependency rubric: kernel/no_std additions require an explicit compatibility check that core/alloc paths do not regress to std through default feature drift, and class ownership is recorded against docs/trusted-build-inputs.md.
• Boot/build input pinning: pin external bootloader/tool downloads to an auditable revision or checksum. Branch names are not enough for TCB inputs. CI should fail when generated capnp bindings or no-std patching change outside an intentional schema/codegen update.
• Untrusted-path panic audit: panic!, assert!, .unwrap(), and .expect() are acceptable during bring-up, but every path reachable from manifest bytes, ELF bytes, SQEs, params buffers, result buffers, and future IPC messages needs either a fail-closed error or a documented halt policy.
• Hardware protection smoke tests: boot under QEMU with SMEP/SMAP-capable CPU flags and assert CR4.SMEP/CR4.SMAP once paging is initialized. Every explicit user-memory dereference must be wrapped in a short STAC/CLAC window once SMAP is enabled.

Tier 2 – Targeted dynamic analysis

Aimed at the host-testable pure-logic crates (capos-lib, capos-config) where the Rust toolchain just works. No kernel changes required.

• Miri on the cargo test-lib and cargo test-config suites. Catches UB in pure-logic code: invalid pointer arithmetic, uninitialized reads, bad provenance, unsound unsafe. The FrameBitmap and CapTable tests in particular push against slot indexing, generation counters, and raw &mut [u8] handling – exactly what miri is good at.
• proptest (or quickcheck) on:
  • capos-lib::elf::parse – random bytes / random perturbations of a valid header must never panic and must refuse anything that isn’t a correctly formed user-half ELF64.
  • capos-lib::frame_bitmap – interleaved sequences of alloc, alloc_contiguous, free, mark_used preserve the invariant free_count == popcount(bitmap == 0) and never double-free.
  • capos-lib::cap_table – insert/remove/lookup sequences preserve “every returned id resolves to its insertion-time object, and stale ids are rejected.”
  • capos-config::manifest encode/decode round trip on arbitrary manifests.
• cargo fuzz harnesses (libFuzzer) on the same three parsers: elf::parse, manifest::decode, and the ring SQE decoder that will land as part of IPC. These run outside CI (they never terminate) but should have a seed corpus checked into fuzz/corpus/ and be run for a fixed budget nightly or on-demand.
• Sanitizers on host tests: RUSTFLAGS=-Zsanitizer=address (and thread) on cargo test-lib under nightly. Requires nothing more than a CI job; cheap to add.

Tier 3 – Concurrency model checking

The capability ring is a lock-free single-producer / single-consumer protocol using volatile reads, release/acquire fences, and a shared head/ tail pair. It is the most likely source of subtle memory-ordering bugs and is also the most isolated – a perfect fit for model checking.

• Loom on a host-buildable wrapper of the ring protocol. Extract the producer/consumer state machine from capos-config::ring into a form where atomics can be swapped for loom::sync::atomic, and write Loom tests that enumerate all interleavings of producer/consumer for small ring sizes (2–4 slots). Properties to check:
  • No CQE is lost.
  • No CQE is double-delivered.
  • The sq_head/sq_tail and cq_head/cq_tail pointers never observe a state that implies tail - head > SQ_ENTRIES.
  • The “corrupted producer state” fail-closed policy (REVIEW_FINDINGS.md “Userspace Ring Client”) holds under adversarial interleavings.
• Shuttle as a lighter alternative for regression-style tests once the specific bugs are known; cheaper per run, randomised rather than exhaustive. Good for long-running overnight jobs.

Loom coverage here is disproportionately valuable: it substitutes for the SMP-hardness work the project has explicitly deferred, and it exercises exactly the ordering that TOCTOU-style bugs hide in.

Tier 4 – Bounded verification of specific invariants

Not a full-kernel proof. Targeted, property-specific, one-module-at-a-time.

• Kani (bounded model checking for Rust, via CBMC). Good fit for small, heap-free, arithmetic-heavy functions. Candidate modules:
  • capos-lib::cap_table – prove that for all insert; remove; insert' sequences under a u8 generation counter, a stale CapId never resolves. Bound: table size ≤ 4, generation window ≤ 256.
  • capos-lib::frame_bitmap – prove that for all bitmap sizes up to N bytes, alloc_frame followed by free_frame of the same frame restores the original bitmap and free_count.
  • capos-lib::elf::parse bounds checks: prove that every index into the program header table is < len, given the validated phentsize and phnum.
• Verus (SMT-based Rust verifier, active development at MSR) for invariants that Kani can’t handle ergonomically, particularly those involving loops and ghost state. Worth tracking but don’t commit to it yet – the proof-engineering cost is real, and the tool is still young. Revisit once IPC lands and the kernel has stable public APIs.
• Creusot / Prusti are alternatives in the same space. Do not invest in more than one SMT-based verifier; pick whichever has the best story for no_std + alloc code when Tier 4 starts.

Deliberately out of scope: Isabelle/HOL, Coq proofs, Frama-C. They would require re-encoding Rust in a foreign semantic framework with no established Rust front-end mature enough for kernel code.

4. Security Review Process

REVIEW.md is the rules document and REVIEW_FINDINGS.md is the open-issue log. REVIEW.md contains the common security checklist that applies across kernel, userspace, host tooling, generators, and CI. The per-boundary prompts below are an expansion of that common checklist for OS-specific code paths.

CWE/CAPEC tagging policy

Security findings should carry CWE metadata when the mapping is specific enough to help a reviewer or future audit. Do not force a CWE into every title.

• Prefer Base/Variant CWE IDs when the root cause is known: CWE-770 for unbounded allocation, CWE-88 for argument injection, CWE-367 for a concrete validation-to-use race, CWE-416 for a real use-after-free.
• Use Class IDs as temporary or umbrella labels: CWE-20 for “input was not validated enough” before the missing property is known; CWE-400 for general resource exhaustion only when the enabling mistake is not more precise.
• Use capability-kernel invariants instead of weak CWE mappings for design properties such as “no ambient authority”, “cap transfer happens exactly once”, “revocation cannot leave stale authority”, and “scheduling context donation cannot fabricate CPU authority”. Cite CWE-862/CWE-863 only when the issue is actually a missing or incorrect authorization check.
• Use CAPEC for the attacker pattern when useful: input manipulation, command injection, race exploitation, flooding, or path/file manipulation. CAPEC is not a substitute for the CWE root-cause tag.

Current checklist coverage:

Per-boundary review checklist

• Syscall surface change (arch/x86_64/syscall.rs):
  • Every register-passed argument is treated as attacker-controlled.
  • No user pointer is dereferenced without validate_user_buffer.
  • Numeric conversions, copy lengths, and pointer arithmetic are checked before constructing slices or entering a UserAccessGuard scope.
  • Kernel stack pointer and TSS.RSP0 invariants are preserved.
  • The syscall count stays bounded; a new syscall has an SQE-opcode alternative considered and explicitly rejected with rationale.
• Ring dispatch change (kernel/src/cap/ring.rs):
  • SQ bounds check and per-dispatch SQE limit still enforced.
  • Corrupted SQ state fails closed (never re-processes the same bad state on the next tick).
  • No allocation in the interrupt-driven path beyond what is already documented in REVIEW_FINDINGS.md.
  • Result buffers and endpoint scratch buffers cannot leak stale bytes beyond the returned completion length.
• User buffer validation change (kernel/src/mem/validate.rs):
  • Address range check precedes PTE walk.
  • PTE flags checked: present, user, and write (if the buffer is written).
  • Single-CPU assumption explicit; TOCTOU note retained until SMP lands.
• ELF loader change (capos-lib::elf):
  • Every field bounded before use (phentsize, phnum, p_offset, p_filesz, p_memsz, p_vaddr).
  • Segments confined to the user half.
  • Overlap check preserved.
  • Integer arithmetic uses checked add/subtract before deriving mapped addresses, file slices, or zero-fill ranges.
• Manifest change (capos-config::manifest):
  • Every optional field is either present or the service is rejected.
  • Name / binary / cap source strings are length-bounded.
  • Unknown / unsupported numbers in CUE input fail-closed with a path- specific error.
  • Capability grants are checked as an authority graph before any rejected graph can start a service.
• Schema change (schema/capos.capnp):
  • Backward-compatible with existing wire format, or migration documented.
  • Every new method has an explicit capability-granting story (who mints the cap that lets this method be called?).
  • Generated code no_std patching still applies.
• Host tool or generator change (tools/*, build.rs, CI scripts):
  • Manifest/config-derived paths cannot escape intended directories through absolute paths, traversal, symlinks, or file-type confusion.
  • External command execution uses explicit binaries and argument APIs, not shell interpolation of untrusted strings.
  • Generated outputs are review-visible and fail closed on malformed inputs.
  • Generated files and diagnostics do not disclose secrets, absolute paths, or stale build outputs beyond what the developer intentionally requested.
• Unsafe block added or expanded: Tier 1 clippy lints plus REVIEW.md §“Unsafe Usage” checklist already cover this; the review should cite the specific invariant being maintained in the commit message.

Threat-model refresh

On every stage completion (Stage 6 IPC, Stage 7 SMP, first driver landing, first time a manifest comes from outside the repo), re-run §2 of this document and update it. The list of trust boundaries grows over time; the proposal decays if it doesn’t grow with the code.

Periodic full audit

Once per stage, schedule a focused audit pass:

1. Re-verify every boundary’s code is still enforced at its documented entry point (no new bypass path).
2. Re-run all Tier 2/3 jobs with the latest toolchain (catches tool-upgrade regressions).
3. Walk through open items in REVIEW_FINDINGS.md and confirm each is still correctly classified (still open, fixed, or explicitly accepted).
4. Record the audit date + outcome at the top of REVIEW_FINDINGS.md, matching the existing “Last verification” convention.

5. Concrete Verification Targets

Ordered by value and feasibility. Each one is a specific, bounded piece of work a contributor can pick up without needing to redesign the kernel.

Targets 1–4 are feasible today and should be the first batch of work. Target 10 is the security gate before treating Stage 6 services as untrusted. Targets 11–12 should be designed before capability transfer lands, otherwise the first IPC implementation will bake in ambient resource authority. Target 14 gates user-mode or semi-trusted drivers.

Current status as of 2026-04-21:

• Targets 1–2 have initial Kani coverage in capos-lib.
• Target 3 has arbitrary-input proptest coverage and a cargo-fuzz target for ELF bytes. The current Kani harness still only proves the short-input early-reject path because fully symbolic ELF parsing reaches allocator and sort internals before there is a sharper proof obligation.
• Target 4 has cargo-fuzz coverage for manifest decoding/roundtrip and mkmanifest exported-JSON conversion.
• Target 5 has a feature-gated Loom model for the shared ring protocol.
• Target 13 has an initial CI baseline plus generated-code drift checking, dependency audit/deny gates, and required QEMU boot still open.

6. Phased Plan

This slots into WORKPLAN.md as a cross-cutting track rather than a phase – items are independent of Stage 6 IPC and can proceed in parallel.

• Track S.1 – CI bootstrap – landed 2026-04-21
  • .github/workflows/ci.yml: fmt-check, test-config, test-ring-loom, test-lib, test-mkmanifest, cargo build --features qemu, make capos-rt-check, generated-code drift checking, and dependency policy checking.
  • QEMU smoke installs build-essential, capnproto, qemu-system-x86, xorriso, and cue v0.16.0 before running make and make run; it remains optional/non-blocking until boot runtime is stable enough to make it a required gate.
  • Clippy-with-deny and cargo-geiger remain future hardening jobs.
• Track S.2 – Miri + proptest on capos-lib – landed 2026-04-21
  • Add proptest dev-dependency to capos-lib.
  • Host properties for capos-lib::cap_table and capos-lib::frame_bitmap; ELF arbitrary-input coverage remains open under S.13.
  • cargo test-lib runs the native host suite; cargo miri-lib runs the same crate under Miri.
• Track S.3 – Manifest + mkmanifest fuzzing – landed 2026-04-21
  • fuzz/ crate with harnesses for manifest::decode and tools/mkmanifest CUE → capnp pipeline. Seed corpus checked in.
• Track S.4 – Ring Loom harness – landed 2026-04-21
  • Extract the SPSC protocol from capos-config::ring into a test-only wrapper where atomics are swappable.
  • Loom tests covering corruption, overflow, and ordering.
  • Doubles as regression coverage for Phase 1.5 in WORKPLAN.md.
• Track S.5 – Kani on capos-lib – initial harnesses landed 2026-04-21
  • CapTable generation/index/stale-reference invariants.
  • FrameBitmap alloc/free symmetry over a small symbolic bitmap model plus a concrete bounded contiguous-allocation proof.
  • ELF parser short-input early-reject panic-freedom.
  • The current bounds are intentionally conservative so make kani-lib remains a practical gate; broader symbolic ELF and contiguous-allocation proofs should wait for more specific invariants.
• Track S.6 – Security review docs stay aligned
  • Keep REVIEW.md’s common security checklist aligned with §4’s boundary prompts as new boundaries land.
  • Add a “threat model refresh” step to the stage-completion workflow in CLAUDE.md.
• Track S.7 – Stage-6-aware refresh
  • Re-run §2 trust-boundary inventory after capability transfer/release semantics land.
  • Plan Loom coverage for cross-process routing and direct-switch IPC.
• Track S.8 – Untrusted-service hardening gate
  • Wire SMEP/SMAP enablement into x86_64 init after paging is live.
  • Replace raw user-slice construction in syscall/ring paths with checked copy/access helpers that bracket the actual access with STAC/CLAC.
  • Add QEMU hostile-userspace tests for bad pointers, kernel-half pointers, invalid caps, corrupted rings, and services without Console authority.
  • Audit untrusted-input paths for panics before Stage 6 endpoints run mutually-untrusting processes.
• Track S.9 – Authority graph and resource accounting – landed 2026-04-21
  • Concrete design is captured in docs/authority-accounting-transfer-design.md.
  • Defines authority graph invariants, per-process quota ledger (cap slots, endpoint queue, outstanding calls, scratch, frame grants, log volume, CPU budget), diagnostic aggregation, and exactly-once transfer/rollback semantics.
  • Establishes acceptance criteria that gate WORKPLAN 3.6 capability transfer and 5.2 ProcessSpawner implementation.
• Track S.10 – Supply-chain and generated-code TCB
  • Pin Limine and other external build inputs by revision/checksum rather than branch name.
  • Make capnp generated-code changes review-visible in CI, including the no-std patching step.
  • Consider cargo-vet only after cargo-deny/cargo-audit are in place; vetting too early is process theater.
  • S.10.3 adds a concrete dependency policy: no_std additions are accepted only with class attribution, cargo deny + cargo audit, and explicit lockfile intent.
  • S.10.3 enforcement is make dependency-policy-check, backed by deny.toml and pinned CI installs of cargo-deny 0.19.4 and cargo-audit 0.22.1.
• Track S.11 – Device/DMA isolation gate
  • Before PCI/virtio/NVMe/user drivers land, choose the DMA isolation story: IOMMU-backed DMA domains or kernel-owned bounce buffers.
  • Define DMAPool, DeviceMmio, and Interrupt capability invariants: bounded physical ranges, explicit interrupt ownership, device reset on revoke, and no raw physical-address grants to untrusted drivers.
  • S.11.2 requires a concrete ownership-transition gate before userspace NIC/ block drivers are allowed.
• Track S.12 – Kani harness bounds refresh
  • Revisit Kani bounds and harness shape once capability transfer, resource-accounting, or validate_user_buffer exposes concrete proof obligations.
  • Prefer actionably narrow properties over arbitrary symbolic parser exploration that spends verifier time in allocator or sort internals.
• Track S.13 – ELF parser arbitrary-input coverage
  • Add proptest coverage for capos-lib::elf::parse on arbitrary bytes and valid-header perturbations.
  • Add a cargo fuzz target for ELF bytes once the corpus and runtime budget are defined.

Tracks S.1 through S.5 have initial coverage. S.6 is ongoing doc hygiene and should move with review-process changes. S.8 must land before Stage 6 runs mutually-untrusting services. S.9 design is complete and now gates concrete implementation work in 3.6/5.2. S.11 gates device-driver work. S.12 should not expand bounds for their own sake; it is a refresh point when new kernel invariants make better proof targets available. S.13 closes the remaining target-3 gap from the table above.

7. What This Proposal Does Not Promise

• No claim that capOS will be “secure” at the end. It will be harder to write a silently wrong change to the code paths the tooling covers, and it will be easier to find the ones that are still wrong.
• No proof obligation on every PR. Kani and Loom are expensive to run on every push; CI runs them on a reduced schedule (e.g. nightly, or on PRs that touch the covered crates).
• Userspace and host-tool bugs are in scope, but their impact is classified by boundary. A userspace bug should not compromise kernel isolation; a host-tool bug can still compromise the build TCB or developer/CI filesystem.
• No claim that confidentiality is handled beyond architectural isolation. Timing channels, cache side channels, device side channels, and covert channels through shared services remain explicit research topics, not current implementation goals.

8. Relation to Other Docs

• docs/research/sel4.md §1 and §6.1 already make the case that full verification is not the right goal. This proposal is the operational answer.
• REVIEW.md is the reviewer’s rulebook. This proposal explains the security and verification rationale behind its common checklist and per-boundary prompts.
• REVIEW_FINDINGS.md is the open-issue log. This proposal feeds it – every bug found by Tier 2/3/4 tooling lands there unless fixed in the same change.
• ROADMAP.md owns the stages; this proposal does not add stages, only a cross-cutting track that runs alongside them.
• WORKPLAN.md owns concrete ordering; Track S.1–S.11 above is the actionable slice mirrored there.