µKernel — Secure by Design

01 — Why µKernel

Security isn't a feature. It's the architecture.

Problem Linux can't be certified. Your DER won't sign off on 30 million lines of C in the safety partition. You're stuck running Linux in a VM on top of a certified RTOS, paying for both.

µKernel ~5,000 lines of Rust. 617 auditable unsafe blocks. DO-178C DAL C certification evidence in progress. DAL A achievable — MC/DC on 5K lines is a bounded effort, not a multi-year program.

Problem You're paying Wind River for VxWorks, Helix, and certification evidence separately. Per-seat development licenses. Per-unit runtime royalties. Every deployed system increases your COGS.

µKernel One product includes the RTOS, hypervisor, and container runtime. Per-program licensing — your cost doesn't scale with headcount or production volume.

Problem Broadcom killed your VMware licenses. Your datacenter hypervisor is now a liability. You need VM hosting, but you also need containers, and your security team wants partitioning.

µKernel Built-in Type-1 hypervisor with Hyper-V enlightenments and virtio. Native POSIX container runtime without a guest OS underneath. Hardware-enforced domain isolation via NPT.

Problem Your embedded team writes Rust. There's no certified Rust RTOS. You're writing Rust applications on top of a C kernel and hoping the FFI boundary doesn't introduce the bugs Rust was supposed to prevent.

µKernel Rust from the kernel up. The compiler eliminates memory safety bugs in the kernel, not just in your application. Every unsafe block is audited, justified, and tracked by CI.

Problem Your RTOS vendor is foreign-owned. NDAA due diligence requires tracing the ownership chain. Aptiv is Irish-domiciled. BlackBerry is Canadian. Your compliance team is asking questions.

µKernel American company. American developer. No foreign code in the TCB. No foreign dependencies. The LLVM toolchain is US-based. The entire supply chain is auditable.

03 — Architecture

One binary. Everything inside.

The certified boundary is three Rust crates enforced by the build system. The hypervisor, container runtime, and dataplane run outside the TCB under kernel supervision.

CERTIFIED TCB 617 unsafe blocks sys-kernel 186 unsafes 15 syscalls, capabilities, IPC, scheduler sys-hal 385 unsafes MMIO, MSR, NPT, SVM/VMX, ARM Stage 2 sys-traits 46 unsafes Cross-platform trait interfaces ──────────────────────────────────────────────────────────────── OUTSIDE TCB Under kernel supervision sys-vmm 394 unsafes Type-1 hypervisor (VM lifecycle, device emulation) POSIX shim ~100 syscalls Container runtime (Linux ABI translation) Dataplane VPP-class packet forwarding Domains Customer workloads (VMs, containers, applications)

	VxWorks + Helix	INTEGRITY	µKernel
Language	C	C	Rust
Kernel LOC	~500,000	~10,000	~5,000
Unsafe Audit	N/A (all C)	N/A (all C)	617 blocks
Hypervisor	Helix (separate license)	Separate product	Built-in
Containers	Linux VM required	Linux VM required	Native POSIX domain
Certification	DAL A	DAL A	DAL C (in progress)
Partitioning	ARINC 653	MILS	CBS + NPT
Ownership	Aptiv PLC (Ireland)	Green Hills Software	American
License	Per-seat + unit + Helix	Per-seat + unit	Per-program

04 — Markets

Where it runs

Aerospace & Defense

Autonomous UAS, mission computers, satellite processors. ARINC 653-class partitioning. NDAA compliant. DO-178C certifiable to DAL A.

Enterprise Infrastructure

Hyperconverged appliances, security gateways, container platforms. VPP-class dataplane at wire speed. VMware and VxWorks replacement.

Industrial & Embedded

CNC controllers, robotics, medical devices, automotive ECUs. Deterministic real-time scheduling on commodity ARM and x86 hardware.

05 — Certification

Designed for certification. Not retrofitted.

The small TCB, Rust type system, and CI-enforced safety gates reduce certification cost by 50% or more compared to a legacy C RTOS.

Common Criteria

Target: EAL4+ (NDcPP v3.0e + Virtualization PP)
TOE: sys-kernel + sys-hal + sys-traits
Evidence: Security Target, ADV/ATE/AVA documentation
Status: In progress

DO-178C

Target: DAL C (statement + decision coverage)
Scope: Microkernel TCB (617 unsafe blocks)
Evidence: PSAC, SRD, SDD, SVP, traceability matrix
Status: First drafts complete

DAL A available as a customer-funded upgrade. MC/DC coverage on 5,000 lines of Rust is achievable. Contact us for scoping.

06 — Licensing

Simple licensing. No surprises.

Per-program licensing. Your cost doesn't scale with headcount or production volume.

Development License

Per-Seat

Full source access under NDA. Build, test, integrate. 12 months of updates and engineering support.

Runtime License

Per-Unit or Per-Program

Deploy µKernel on production hardware. Per-program terms available for high-volume platforms.

BSP License

Per-Platform

Board support package for TI TDA4VM, x86 reference, and custom hardware targets.

Certification Evidence

Per-Program Per-Architecture

DO-178C DAL C evidence package. Produced once, licensed independently per program.

Secure by design.