Secure systems engineering is shaped less by microkernel architecture itself than by the tension between maximal assurance and practical evolvability. Formally verified microkernels (e.g., seL4) deliver machine-checked correctness at substantial verification cost, while production kernels (e.g., Zircon) prioritize scalability and feature velocity, typically expanding the trusted computing base. This paper presents NEURON, a compact Rust-based capability microkernel for RISC-V, as a reference implementation exploring a pragmatic middle ground. NEURON combines (1) compile-time structural guarantees via Rust’s ownership and type system, (2) deterministic operational discipline through bounded resources and explicit backpressure, and (3) ownership-safe SMP scheduling with per-CPU run queues and bounded QoS-respecting work stealing. Inline IPC frames are bounded by the kernel ABI to 8 KiB (8192 bytes); independently, many user-space service protocols adopt a 512-byte reply/frame convention as a protocol choice rather than a kernel limit. Rather than claiming full formal correctness, the design targets structural safety, bounded state growth, and reproducible control-path behavior. Evaluation on host tests and QEMU selftests shows bounded runnable growth under saturation, structural enforcement of WX mapping invariants, deterministic scheduling behavior under controlled conditions, and observable SMP rescheduling contracts via evidence counters. These results suggest that type-level enforcement paired with deterministic construction practices can yield substantial robustness benefits while preserving implementation flexibility—positioning NEURON between proof-heavy minimalism and large-scale production kernels.
Jenning Schäfer (Tue,) studied this question.