feat(native-kernel): bare-metal capability microkernel skeleton (M1–M5) - #1317
Draft
joshuajbouw wants to merge 16 commits into
Draft
feat(native-kernel): bare-metal capability microkernel skeleton (M1–M5)#1317joshuajbouw wants to merge 16 commits into
joshuajbouw wants to merge 16 commits into
Conversation
Isolated cargo workspace (members crates/* + tools/*) pinned to stable 1.95.0 with the x86_64-unknown-none target. Ring-0 profile: opt-level 2, panic=abort. Nested [workspace] auto-excludes from the surrounding core workspace. Claude-Session: https://claude.ai/code/session_01Bvhtit6VywvsU3nPFU7tZS
bootloader_api entry_point with a fixed physical-memory mapping and 128 KiB stack; polled COM1 UART; monotonic seq counter and serial writer behind one interrupt-safe spinlock; isa-debug-exit halt path. Events are compile-time literals only (legibility-ABI seed). Claude-Session: https://claude.ai/code/session_01Bvhtit6VywvsU3nPFU7tZS
Bitmap frame allocator over 256 MiB (fallible alloc_frame/free_frame, bounded by construction); linked_list_allocator Heap used directly (no global_allocator); live page-table walk auditing .text/.rodata/data W^X, reporting reality. Claude-Session: https://claude.ai/code/session_01Bvhtit6VywvsU3nPFU7tZS
Full architectural-exception IDT installed via the stable Entry::set_handler_addr path (the nightly x86-interrupt ABI is unavailable on pinned stable 1.95.0), so each vector is a naked-function stub calling one C-ABI trap handler. Structured fault event per exception; page-fault RIP-fixup recovery; double fault on a dedicated 16 KiB IST stack via GDT/TSS. Claude-Session: https://claude.ai/code/session_01Bvhtit6VywvsU3nPFU7tZS
Legacy PIC remapped and fully masked; local xAPIC enabled via MMIO; periodic timer emits ticks 1..=8 then masks. RDRAND CPUID-gated: entropy.seeded on success, entropy.unavailable otherwise, never a silent PRNG fallback. Claude-Session: https://claude.ai/code/session_01Bvhtit6VywvsU3nPFU7tZS
Self-tests (W^X write fault, NX exec fault, heap/frame exhaustion return fallibly, int3 handled, frame reuse positive control), each emitting test.pass/fail. kimage wraps the kernel ELF into a UEFI image; ktest builds, determinism-checks (blake3 x2), boots under the frozen QEMU contract with a 120 s hard kill, and asserts the JSONL evidence. Claude-Session: https://claude.ai/code/session_01Bvhtit6VywvsU3nPFU7tZS
…te name The ring-0 artifact takes the name charter §9 reserves for it, removing the collision with the user-space astrid-kernel semantic supervisor. Claude-Session: https://claude.ai/code/session_01Bvhtit6VywvsU3nPFU7tZS
Add the first ring-3 protection domain to the M1 skeleton: per-domain page tables (own PML4, kernel higher-half copied without USER, user code RX / stack RW+NX by construction), syscall/sysret entry via EFER.SCE+STAR/LSTAR/SFMASK, an xv6-style scheduler continuation so enter_user returns a RunOutcome, tick-quota preemption (ADR-K6 seed), fault/quota kill with full frame reclamation checked against a live allocator free-frame census, and the ADR-K2 capability table with generation-based O(1) revocation (ADR-K4). Seven kernel-driven scenarios prove it end to end: happy path, kernel-read page fault, privileged-instruction #GP, BadCap, stale-cap after revocation, quota kill of a runaway loop, and clean pool reuse. All M1 self-tests and events keep passing (M2 is a superset). Claude-Session: https://claude.ai/code/session_01Bvhtit6VywvsU3nPFU7tZS
Extend the serial-assertion harness with the M2 superset: all seven ring3_* test.pass names, a domain.killed for each cause literal (pf/gp/quota), cap.revoked presence, one balanced domain.reclaimed per domain.create, and the final halt gate. Raise the QEMU hard timeout to 180s for the preemption run. Claude-Session: https://claude.ai/code/session_01Bvhtit6VywvsU3nPFU7tZS
…y derivation
Extend the ring-3 substrate from one run-to-completion domain (M2) to two
coexisting domains communicating over bounded IPC endpoints, with capability
transfer by derivation (ADR-K3) and scoped subtree revocation (ADR-K4).
Load-bearing new mechanism: suspend/resume of a ring-3 domain at a syscall
boundary. A `recv` on an empty endpoint captures the user continuation
(user_rip/user_rsp) straight from the SyscallFrame, sets the domain Blocked,
and returns to a tiny round-robin scheduler via a new OUT_BLOCKED tag. Resume
is a fresh context_enter at the saved continuation with the delivered
(status, data) placed in rax/rdx. `context_enter` gains entry_rax/entry_rdx;
every other GP register is still zeroed (M2 infoleak defense preserved). ABI
rule: a blocking `recv` may clobber all registers except its rax/rdx return.
- syscall.rs: generalize context_enter(+entry_rax,+entry_rdx); add OUT_BLOCKED;
dispatch syscalls 4 ep_create, 5 send, 6 recv, 7 revoke_tree.
- domain.rs: State::Blocked; bounded ENDPOINTS[16] (queue depth 4) and DERIV[128]
pools as single stores; ObjectClass::Endpoint(slot) as the only object->endpoint
link; CapEntry.deriv_node becomes live machinery; check_cap gains the deriv
liveness step (Revoked -6); new status FULL -5, NO_RESOURCE -7; monotonic-shrink
transfer with lazy root + child derivation nodes (no partial state on failure);
scoped revoke_tree (single bounded pass); a real scheduler_run with a 256-step
budget, deadlock detection (Cause/KillCause::Deadlock), and the seven IPC
scenarios. Baseline census emitted at the M2->M3 boundary so the M1/M2 serial
stream stays byte-identical.
- serial.rs: ep.create, ipc.{send,recv,blocked,wakeup,cap_dropped}, cap.transfer,
cap.revoke_tree, ipc.deadlock, pools.census events.
- payloads.rs: 12 M3 ring-3 payloads; document the blocking-ABI clobber rule.
All M1 self-tests and M2 scenarios keep passing byte-identically (M3 is a strict
superset). cargo fmt + clippy -D warnings clean on x86_64-unknown-none.
Claude-Session: https://claude.ai/code/session_01Bvhtit6VywvsU3nPFU7tZS
Assert the seven M3 scenario test.pass names plus: ipc.blocked before ipc.wakeup (suspend/resume), cap.transfer with rights=3 and rights=1 (transfer-by-derivation + monotonic shrink), cap.revoke_tree killed>=2 (scoped subtree revocation), ipc.deadlock + domain.killed cause=deadlock (liveness guard), and final pools.census == baseline (no object/endpoint/ deriv-node leak). Bump the QEMU wall-clock timeout to 240s. All existing M1/M2 assertions retained unchanged. Claude-Session: https://claude.ai/code/session_01Bvhtit6VywvsU3nPFU7tZS
…deltas, reasoner The kernel serializes its five live object tables as typed, versioned, integer-columned relations (REL_DOMAIN/OBJECT/CAPABILITY/ENDPOINT/DERIVATION), computed by reading the live tables at enumerate time — SINGLE STORE, no second fact base (Barrelfish lesson). Deltas are typed projections emitted from the same mutation sites, gated on the single bounded subscriber; subscribe primes the fold with the current snapshot as add deltas. New: ObjectClass::Legible + LEGIBLE_READ right (capability-gated, revocable via the exact ADR-K2 check_cap order); syscalls 8-12 (legible_schema/enumerate/ subscribe/get, cap_object); five ring-3/ring-0 scenarios including the ring-3 reasoner that counts, from relation rows alone, the capabilities referencing its own transferred object. v0 is timing-free row-granular; per-relation scoping and per-subscriber IPC delivery deferred. All M1/M2/M3 seq values byte-identical (deltas emit nothing without a subscriber; M4 appends after the M3 census). Claude-Session: https://claude.ai/code/session_01Bvhtit6VywvsU3nPFU7tZS
Fold every legible.delta within the check.begin/check.end window into a per-relation model keyed by subject key, independently collect the enumerate snapshot rows, and require the two row sets EQUAL for every relation (LEGIBILITY DRIFT otherwise) — the fold done in host Rust so the check is independent of the kernel's bookkeeping. Also cross-check every legible.schema against the frozen column-code table, verify begin/end framing (row count == end.rows, frozen arity), the five M4 test.pass, and the unauthorized-enumerate legible.denied. QEMU timeout bumped to 300s. Claude-Session: https://claude.ai/code/session_01Bvhtit6VywvsU3nPFU7tZS
…root Ring 0 assigns a gapless monotonic audit_seq to authority-changing actions and maintains a BLAKE3 rolling root (root' = blake3(prev32 || canonical40)) over a bounded 256-record log. Seven audit kinds (domain create/kill, cap mint/transfer/ revoke, revoke-tree, ep create) are appended from the SAME sites that already emit the serial ev_* events, so a record cannot diverge from its action. Ring 0 hashes but never signs and never parses a record (charter §2/§7). The append path is a single atomic-load fast-return unless AUDIT_ARMED, which is flipped only at the start of the M5 scenario block — so M1-M4 emit nothing new and their serial seq stream stays byte-identical. New capability-gated syscalls 13-16 (audit_len/root/get/enumerate) read the chain behind a new ObjectClass:: Audit + AUDIT_READ gate (right AND object-class == Audit, mirroring legibility). Four appended scenarios: audit_orders_and_roots (fixed script over all kinds + real IPC transfer, exact-count + non-zero-root assert), audit_gated (unauthorized denied + audit.denied, authorized OK), audit_chain_verifies (emits the full canonical stream for host-side crypto reconstruction), audit_light_tenant (a ring-3 asm auditor doing the LIGHT non-crypto check it can — len + first-kind; full in-guest BLAKE3/ed25519 is deferred to a Wasmtime tenant). blake3 rides the pure feature (portable core) so it links on the SSE-less bare-metal target. Claude-Session: https://claude.ai/code/session_01Bvhtit6VywvsU3nPFU7tZS
The host harness is ADR-K7's user-space verifier stand-in. It dedups the emitted audit.record stream by audit_seq, reconstructs the BLAKE3 rolling root from the frozen genesis using the SAME blake3(prev32 || canonical40) rule, and asserts it equals ring 0's final audit.root; ed25519-signs the recomputed head with a fixed- seed host keypair and verifies the round-trip; then flips one record byte and asserts the root diverges (tamper-evident). Prints the three audit-chain sub- checks and gates on all three. Adds the M5 assertion block: the four scenario test.pass names, audit_seq gapless 0..len over the enumerated stream, audit.denied present, and the audit-chain host verification. ed25519-dalek is a host-tool dependency only; QEMU timeout bumped to 360s. Cargo.lock updated (--locked clean). Claude-Session: https://claude.ai/code/session_01Bvhtit6VywvsU3nPFU7tZS
joshuajbouw
added
the
large-file-ok
75 tasks
joshuajbouw
added a commit
that referenced
this pull request
Aug 24, 2026
Successor of 0b07d42. The signed original head is preserved. ktest now requires contiguous strictly increasing seq from 0, terminal halt, rejection of every test.fail including unknown names, and required M1 events exactly once. Host regressions falsify the original head on a sequence gap/reorder/duplicate, a post-halt event, and test.fail name=future_gate. Firmware discovery documents that QEMU 11.0.2 does not support -print-datadir; that probe is used only when the binary accepts it. This run's evidence is executable-relative share, package prefix, and env override. Do not claim datadir portability. kernel/check.sh runs the supported split checks: stable ktest test/clippy, stable astrid-native-kernel clippy for x86_64-unknown-none, and nightly kimage clippy with isolated target dirs. Do not claim generic workspace clippy. Changelog fragment granted at changes/1564.added.md. Image determinism remains FAIL. No KVM, virtio/IOMMU, DMA, bare-metal/no-host, physical ownership, dual-closure, A/B, first-owner, Wasmtime, filesystem, Linux, or Hermes claim. Context: #1564 (T1 M1 AMEND successor). Inventory: #1317. Signed-off-by: Joshua J. Bouw <jjb@unicity-labs.com> Assisted-by: OpenAI Codex: Grok 4.6
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Linked Issue
Closes #1316
Summary
The first executable proof of the kernel charter's design intentions: a freestanding
x86_64-unknown-nonecapability microkernel that boots under UEFI/QEMU and demonstrates the charter's security and AI-native properties against real hardware behaviour, each asserted by a machine-readable serial-event harness. This is an isolatedkernel/Cargo workspace — it is not built by core CI, its ownCargo.lock/toolchain are separate, and no production code path depends on it. Draft for review of the approach and the design-to-evidence mapping, not for merge.Changes
#[global_allocator]), W^X audited from the live page tables, negative-first self-tests (rodata write / NX exec / heap + frame exhaustion / int3).snapshot == fold(deltas)drift invariant and a ring-3 reasoner deriving a fact from kernel ground truth.Verification
cd kernel && cargo run -p ktestbuilds the ring-0 image, boots it under QEMU (q35/UEFI/TCG) under a hard timeout, and asserts the full serial-event sequence — all self-tests and scenarios pass,halt outcome:"ok", QEMU exit 33.cargo fmt --checkandcargo clippy -D warningsare clean for the ring-0 crate (bare-metal target) and the host tools. All commits are GPG-signed.Honest state / not yet done
bootloadercrate stamps random GPT GUIDs — the kernel ELF is bit-identical; the harness reportsDETERMINISM: FAILnon-gating).bootloader0.11 builder uses-Zbuild-std); the ring-0 kernel itself stays on pinned stable 1.95.Checklist
[Unreleased])cargo metadata)