A bare-metal Rust kernel with runtime-programmable behavior through verified eBPF programs.

Axiom targets robotics and embedded systems where kernel logic should evolve without reflashing firmware. Instead of recompiling to change kernel behavior, verified programs are loaded and attached to kernel hooks at runtime.

Status: research kernel under active hardware bring-up on Raspberry Pi 5. Not production-ready. See Limitations for the current honest list of what works and what doesn't. Benchmarks in docs/benchmarks.md are measured on real hardware; the headline numbers (e.g. 211 ns interrupt latency) are single-core, single-program, no-contention measurements — multi-core RT claims require the scheduler work tracked under issue #57.

Repository structure:

• kernel/src — core kernel implementation
• kernel/crates — modular kernel subsystems (BPF, VFS, etc.)
• userspace/ — userspace programs and libraries
• scripts/ — build system and deployment tools
• docs/ — architecture, benchmarks, protocols — or visit docs

Embedded systems deployed in the field need behavioral updates — new sensor fusion algorithms, modified control loops, updated safety policies. Traditional kernels require full reflash cycles: risky, slow, and capable of bricking devices. Axiom instead hot-loads verified eBPF programs onto kernel hooks (syscalls, timers, GPIO, PWM, IIO) at runtime, detachable on the fly.

This is proven in Linux, but Linux is unsuitable for hard real-time robotics due to unpredictable latency and resource overhead:

The latency figure is honest about its boundary: hardware vector entry → BPF dispatch, single core, no contention. Tail latency under load is not yet measured (#74). Full methodology in docs/benchmarks.md.

Three decisions define the kernel — detail and rationale in docs/architecture.md:

1. Bare metal, monolithic. No host OS, no RTOS. Limine bootloader (x86_64) or device tree (AArch64). Microkernel IPC overhead is unacceptable for control loops; Rust trait boundaries provide the modularity instead.
2. Rust core, no_std, panic=abort. ~95% Rust; assembly limited to boot stubs and exception vectors. Memory-safety bug classes (use-after-free, double-free, data races) are eliminated at compile time; unsafe blocks are explicit and audited.
3. eBPF for runtime extension. Programs are verified, then attached to hooks:

// Loaded at runtime, verified, then attached to GPIO line 23
BPF_PROG(gpio_handler, struct gpio_event *event) {
    if (event->line == 23 && event->rising_edge) {
        sys_wake_task(PID_MOTOR_CONTROLLER);
        metrics.gpio_triggers++;
    }
    return 0;
}

What the verifier guarantees today: bounded execution, constrained stack, validated memory access, termination proof, and a static WCET cycle bound per program from a Pi5-calibrated cost model. The verifier gates the sys_bpf load path — programs that fail do not load. Loads are admission-controlled: a program that can't fit one control-loop period is rejected, and attaches commit wcet × freq against a utilization budget (EDF test, validated on hardware — docs/benchmarks.md §12). Program provenance is authenticated on load (Ed25519, fail-closed; unsigned loads still allowed by default until a userspace signer ships). A libfuzzer harness runs on every PR and nightly.

Execution: interpreter (portable, ~50ns/insn on x86_64) or JIT (AArch64, <5ns overhead), selected per compile-time profile (8KB-stack embedded → 512KB-stack cloud).

Requirements: Rust nightly, cargo, QEMU, cross targets (x86_64-unknown-none, aarch64-unknown-none).

# Build and run in QEMU (x86_64)
cargo run

# RPi5 build (kernel8.img with embedded ext2 rootfs)
./scripts/build-rpi5.sh

Working: boot (x86_64, AArch64); virtual memory + paging; interrupts (APIC, GIC); preemptive scheduling; syscalls; kernel heap; eBPF runtime (interpreter + AArch64 JIT); eBPF verifier gating the load path (CFG, bounds, tnum, pruning, liveness); WCET admission control; BPF signing (enforcement opt-in); VFS + ext2 (read-only); RPi5 GPIO/UART/PWM; VirtIO; shell + basic utilities.

Not yet: RPi5 SPI/I²C, USB, full DMA; POSIX compatibility (partial); RISC-V beyond boot.

The kernel boots and runs real BPF programs on a Raspberry Pi 5. Several load-bearing pieces are not yet in place; pretending otherwise wastes a reader's time.

Kernel core:

• User-mode page faults panic the kernel — there is no signal delivery, so a faulting user task takes the kernel with it (#52, #53)
• No demand paging — every user page is pre-allocated at process creation; brk / mmap don't grow lazily (#54)
• No copy-on-write fork on x86_64 — full page copy; aarch64 path has CoW
• sys_nanosleep busy-spins — wait queues not yet wired (#56)
• No POSIX signals — kill, sigaction, SIGSEGV delivery all absent
• Boot panics on missing /bin/init — no recovery path (#55)

Scheduler:

• Single global run queue across all CPUs — work-stealing + per-CPU queues tracked under #57
• No priority inheritance on kernel mutexes — classic priority inversion possible (#60)
• No preempt_disable / preempt_enable primitive — critical sections either use IRQ-disable or hope (#62)
• EDF scheduling exists for BPF programs only, not for native OS tasks (#61)

BPF subsystem:

• Unsigned loads accepted by default — provenance enforcement is wired (#20) and fails closed on bad signatures, but allow_unsigned = true until a userspace signer ships
• BPF Manager guarded by one global mutex — every map op / load / attach serializes (#58)
• No BPF-to-BPF function calls (#87), no BTF integration (#90), no Spectre mitigations (#89)
• WCET admission assumes one nominal 1 kHz fire rate for every hook — per-hook-type / caller-declared frequencies are future work; PREVAIL head-to-head comparison not yet run

Memory:

• AddressSpace doesn't track per-frame ownership on Drop — long-running systems with process churn slowly leak physical memory (#69)
• Task stack isolation FIXME — stacks in higher half may be cross-writable; security audit pending (#70)

Drivers:

• No I²C, SPI, CAN, or Ethernet drivers today — only GPIO / PWM / UART on the RP1. Tracked under #63, #64, #66, #67
• No hardware watchdog integration (#72)

Operations:

• No persistent crash dump (#73), no A/B kernel slots / rollback (#75), no hardware-in-loop CI — Pi5 testing is manual (#76)

Benchmark caveats:

• The 211 ns interrupt-latency headline is a single-core, single-program, no-contention measurement. Multi-core RT claims require the per-CPU run queue work in #57 plus a 24h soak with P99 / P99.9 histograms (#74).
• The 5.8× boot-time improvement is measured against stock Raspberry Pi OS Linux. A minimal Buildroot Linux on the same hardware closes much of that gap. Honest comparative benchmarks against Zephyr / NuttX / Linux PREEMPT_RT are tracked under #78.

The full picture lives in issue #81 — execution roadmap. If a feature isn't in the list above, treat it as not yet implemented and check the roadmap before relying on it.

Axiom is not a production kernel (yet), not POSIX-compliant (by design), and not a Linux replacement. It is a research platform for runtime kernel extension, exploring:

1. Can eBPF verification provide sufficient safety for kernel extensions?
2. Does Rust's type system meaningfully reduce kernel bugs in practice?
3. What's the performance overhead of safe abstractions in bare-metal contexts?
4. How minimal can a usable kernel be while supporting dynamic behavior?

This is experimental research code. Contributions welcome, especially architecture ports, drivers (USB, DMA, network), eBPF optimizations, and userspace POSIX compatibility.

Code standards: all unsafe blocks need safety comments; public APIs need documentation; tests for verifiable components; benchmark critical paths.

Triple-licensed under MIT, Apache 2.0, and MPL 2.0.

Utkarsh Maurya
GitHub: https://github.com/pro-utkarshM
Email: utkarsh@kernex.sbs

Further reading:

• docs/architecture.md — system layers, execution model, syscall flow, eBPF deep dive, memory management, HAL
• docs/benchmarks.md — authoritative hardware benchmarks (Pi5) and Linux comparison
• kernel_bpf docs — eBPF runtime architecture, scheduling, verification, profiles