Minimalist Microkernels for Mission-Critical Vehicle Compute
Monolithic operating systems with tens of millions of lines of code present intolerable attack surfaces for drive-by-wire vehicles. SDVKernel explores mathematically verified microkernels where only thousands of lines execute in privileged mode.
Shrinking the Trusted Computing Base from Millions of Lines to Ten Thousand
In a monolithic kernel like standard Linux, a crash in a Wi-Fi driver or filesystem brings down the entire vehicle steering controller. In a capability-based microkernel, drivers and filesystems execute as unprivileged user-space processes isolated by Memory Protection Units (MPUs).
Core Engineering Areas
- Formally Verified Microkernels (seL4) — seL4 is the world's first operating system kernel with a complete mathematical proof of functional correctness from high-level specifications down to compiled binary machine instructions.
- User-Space Device Driver Isolation — In classical OS designs, device drivers run inside the kernel. In microkernel architectures, CAN, Ethernet, and PCIe drivers execute as sandboxed user-space processes; if a peripheral bus malfunctions, the driver crashes and restarts without rebooting the vehicle.
- Capability-Based Security — Traditional monolithic automotive kernels grant root-level authority to system services, leaving ECUs vulnerable to privilege escalation. seL4 and verified microkernels use capability-based access control, where every operation requires presenting an unforgeable cryptographic token proving explicit authorization.
Technical Articles