KRN-PART requirements¶
Every thread shall belong to exactly one partition. Rationale: The partition is the unit of accounting, rights, and containment. Status: Accepted 2026-10-07 Verification: Analysis: generator rejects a thread without a partition; the kernel partition is the default in unprotected builds. Trace: SPEC-010 §2; ADR-015 |
Builds without protection hardware shall have exactly one partition and no partition code. Rationale: Footprint of tiny and base. Status: Accepted 2026-10-07 Verification: Footprint test: the partition symbols are absent from tiny and base images. Trace: SPEC-010 §14 |
On protection hardware, memory access of an unprivileged partition shall be limited to its regions; violations shall be partition faults. Rationale: Freedom from interference. Status: Accepted 2026-10-07 Verification: Isolated-profile tests Trace: SPEC-010 §4, §6 |
Partition restart shall not require system reboot and shall restore the partition’s static data to its initial image. Rationale: Recovery of a contained fault while the rest of the system keeps its guarantees. Status: Accepted 2026-10-07 Verification: Test: Trace: SPEC-010 §7 |
Fault policy shall be per partition and applied by a supervisor partition, not hard-coded in the kernel. Rationale: Hubris and Tock: policy outside the kernel keeps the kernel small and the policy testable. Status: Accepted 2026-10-07 Verification: Analysis: the kernel’s fault path only records and notifies; Test: replacing the reference supervisor changes the behavior. Trace: SPEC-010 §6 |
Partition definitions shall be static, build-time data in the first isolated release; dynamic partition creation is FUTURE. Rationale: Static tables are auditable and need no kernel allocator. Status: Accepted 2026-10-07 Verification: Analysis: no runtime partition creation API exists. Trace: SPEC-010 §1, §2 |
In isolated profiles, the kernel state that describes a partition (its threads, objects, wait nodes, capability table) shall live in a kernel-owned sub-region of that partition’s memory, sized by the generator and re-initialized on restart; a partition shall not be able to consume kernel memory outside it. Rationale: ADR-033. Status: Accepted 2026-10-07 Verification: Analysis: generator report lists kstore size per partition; Test: Trace: SPEC-010 §3 |
A partition shall be described by privilege, supervisor, fault policy, restart limit, regions, threads, objects, initial capabilities, capability table size, and optional share; the generator shall emit the partition table, capability tables, descriptors with kstore addresses, device grants, linker sections, and protection tables from it. Rationale: One source of truth for isolation (SPEC-014). Status: Accepted 2026-10-07 Verification: Generator tests Trace: SPEC-010 §2 |
Each partition’s RAM shall be one block with the kstore at its end, privileged-only; code shall be in per-partition flash sections; the generator shall enforce the region count, alignment, size, and kstore-exclusion constraints of the protection hardware and shall fail the build naming the violated constraint. Rationale: Armv7-M’s power-of-two regions and the region budget are the hard part; it belongs to the generator, not to runtime. Status: Accepted 2026-10-07 Verification: Generator tests for Armv7-M and Armv8-M constraint violations; boot test of the isolated reference configuration. Trace: SPEC-010 §3, §4.1, §4.3 |
Only a context switch between threads of different partitions shall reprogram the protection hardware and the privilege bit; switches within a partition shall cost the same as in the base profile. Rationale: Isolation must not tax every switch. Status: Accepted 2026-10-07 Verification: Benchmark: harness switch cost intra- and cross-partition (T5, T12). Trace: SPEC-010 §4.4 |
Every unprivileged thread shall have a kernel stack in its partition’s kstore; a system call shall switch to it and execute the marshaller and implementation in privileged thread mode with interrupts enabled, so that it can block through the wait protocol; the per-CPU exception stack shall be used only for trap entry and exit. Rationale: Blocking is impossible in exception context; the kstore accounts the memory to the partition. Status: Accepted 2026-10-07 Verification: Test: Trace: SPEC-010 §5.2 |
Trap stubs, marshallers, and the syscall table shall be generated from the API annotations with explicit argument-kind classification; the generator shall refuse an unclassifiable prototype; syscall numbers shall be stable within a release line. Rationale: No hand-written wrapper layer (R-001 §7, FreeRTOS); the review gate for new API is the generator. Status: Accepted 2026-10-07 Verification: Generator test with a deliberately unclassifiable prototype; ABI document check in CI. Trace: SPEC-010 §5.3 |
Marshallers shall validate handles through capability lookup with the annotated right, pointer arguments against the caller’s regions with the needed access and bounded length, attribute structs by copy before validation, names by copy into kstore buffers, scalars by range, and callback pointers against executable regions; every failure shall be a status to the caller. Rationale: Attribute snapshots avoid top-level field races; buffer lifetime, nested pointers and safe copies additionally require KRN-PART-025. No unvalidated user pointer (R-001 §7, NuttX). Status: Accepted 2026-10-07 Verification: Test: Trace: SPEC-010 §5.4; KRN-CAP-002 |
Privileged code shall call kernel implementations directly; an ordinary API-entry Rationale: One ordinary calling convention per privilege level; the authenticated internal syscall-return trap is a separate exception (SPEC-010 §5.2, KRN-PART-026). Status: Accepted 2026-10-07 Verification: Test: Trace: SPEC-010 §5.1, §12 |
A fault in an unprivileged thread shall suspend that thread with its state preserved and the Rationale: Containment with the evidence intact for the supervisor and the debugger. Status: Accepted 2026-10-07 Verification: Test: Trace: SPEC-010 §6 |
Restart shall, in order: stop every thread of the partition without delivering results, flush other partitions’ waiters on its objects and threads with Rationale: A defined, auditable sequence that leaves no dangling reference. Status: Accepted 2026-10-07 Verification: Test: Trace: SPEC-010 §7 |
The reference supervisor shall enforce a per-partition restart limit over a window, escalating to the system action when exceeded, and shall wait a configurable minimum delay (default 5 ms) before restarting so that the faulted state can be recorded. Rationale: Hubris’s lesson: a crash loop must be visible, and the evidence must survive it. Status: Accepted 2026-10-07 Verification: Test: Trace: SPEC-010 §6.3 |
The kernel shall offer the supervisor: dequeue of fault descriptors, partition info, suspend, resume, restart, and resumption of a faulted thread for debugging, each gated by the corresponding partition rights; the reference supervisor shall ship as a replaceable subsystem. Rationale: Policy out of the kernel, mechanism in it. Status: Accepted 2026-10-07 Verification: Test: Trace: SPEC-010 §6.3 |
A device capability shall map the device’s MMIO range into the partition and deliver its interrupts as a notification bit on a designated thread after the kernel masks the line; the thread shall unmask with Rationale: Drivers in partitions without kernel code per driver (Hubris, R-001 §7). Status: Accepted 2026-10-07 Verification: Test: Trace: SPEC-010 §8 |
Shared memory between partitions shall be declared at top level with each participant’s permissions and mapped as a region for each; the kernel shall not mediate accesses to it. Rationale: Zero-copy sharing with explicit permissions. Status: Accepted 2026-10-07 Verification: Test: Trace: SPEC-010 §9 |
When partition shares are configured, the kernel shall charge thread execution to the thread’s partition at every switch and deliver share and budget events per ADR-029. Rationale: Temporal protection needs per-partition time. Status: Accepted 2026-10-07 Verification: Test: Trace: SPEC-010 §10; KRN-TP-007 to 009 |
Partition faults, restarts, suspends, resumes, denied capability uses, and delivered interrupts shall be trace events; syscall tracing shall be an option; per-partition statistics shall include syscalls, denials, faults, restarts, and CPU time; the debug descriptor shall export the partition table, kstore layouts, and capability tables; contained faults shall optionally produce retained crash-record entries. Rationale: Containment that cannot be observed cannot be trusted. Status: Accepted 2026-10-07 Verification: Test: trace decoder; descriptor consumer; retained record read-back after a contained fault. Trace: SPEC-010 §13; OBS-005, OBS-008 |
M3 shall implement static partitions, kstores, generated layout and protection tables, cross-partition switching, the syscall boundary, fault delivery, the reference supervisor, restart, device capabilities with interrupt delivery, and shared regions on Armv7-M and Armv8-M; PMP, ports and leases, budget donation, secure partitions, and the trap-free kernel page are deferred. Rationale: The roadmap’s M3 exit criteria (07 §2). Status: Accepted 2026-10-07 Verification: M3 exit review against this list. Trace: SPEC-010 §15; 07 §2 M3 |
An untrusted partition shall not directly program a DMA-capable device unless independent hardware constrains all addresses/descriptors it can use. Otherwise a trusted driver shall validate and own DMA requests. Before partition memory is reset or reused, all asynchronous producers shall be quiesced within a declared deadline or recovery shall escalate. Shared devices shall use per-client cancellation rather than an unrelated global reset. Rationale: CPU protection does not generally constrain bus masters; restart must not leave writes into reused memory. Status: Proposed 2026-10-14; unimplemented. Verification: Planned physical-board negative DMA access tests; fault injection during transfers/restart; stalled-device escalation and shared-client continuity cases. Trace: SPEC-010 §7, §8, §17; KRN-PART-003, 004 |
Marshallers shall check address/length arithmetic without overflow and complete-region permissions, snapshot security-relevant descriptors, and keep mappings, object references and permitted buffer ownership valid until completion or bounded cancellation. Completion shall reject a changed caller incarnation; restart shall remove every in-flight reference to memory it will reuse. Rationale: Entry-time pointer validation alone cannot protect a blocking call or a restarted partition. Status: Proposed 2026-10-14; unimplemented. Verification: Planned range-overflow/hole/permission tests; mutate descriptors after entry; restart/cancel while remote sends or DMA reference user buffers; safe-copy fault recovery tests. Trace: SPEC-010 §5.4, §17; SPEC-007 §2 |
Ordinary user entry and internal privileged syscall return shall be validated as distinct paths. A user shall not forge privileged return state or overwrite arbitrary kstore bytes through object initialization; construction shall be restricted to a kernel-authorized typed slot. Rationale: Protected storage and stacks are ineffective if marshalling permits authority bypass. Status: Proposed 2026-10-14; unimplemented. Verification: Planned forged syscall number/frame/stack tests, nested entry tests, out-of-slot/overlapping init requests and fuzz campaigns. Trace: SPEC-010 §3, §5.2, §17; KRN-PART-011, 013 |
Restart shall declare stop/quiescence and protected-step bounds, preserve incremented incarnation state across image restoration, and complete remote waits with their specified outcomes. A claimed unrelated-partition response-time guarantee shall include priority, locks, bus interference and device stopping; a missed stop deadline shall escalate safely. Rationale: Preemptible steps alone do not establish progress or freedom from interference. Status: Proposed 2026-10-14; unimplemented. Verification: Planned fault/restart campaigns with remote lock owners/waiters, stale handles, DMA and unrelated workload; generation-exhaustion tests; archived physical latency analysis and samples. Trace: SPEC-010 §7, §17; KRN-PART-004, 016; KRN-CAP-013 |