Can a verified microkernel actually secure a car?

In July 2015, two security researchers took control of a Jeep Cherokee while a journalist was driving it on a St. Louis highway. They reached it over the cellular network, through the entertainment system. From there they got onto the vehicle's internal bus and started sending commands to things that steer and stop the car. Chrysler recalled 1.4 million vehicles.

The technically interesting part of that story is not the initial break-in. Head units are complicated internet-connected computers running large amounts of third-party code, and complicated internet-connected computers get broken into. That is a permanent condition, not a bug someone forgot to fix.

The interesting part is what happened next: nothing stopped them. A compromise of the least safety-critical component on the vehicle became a compromise of the most safety-critical ones, because there was no structural reason it couldn't.

This is the problem formally verified microkernels are actually good at. It is worth understanding precisely what they solve, because the gap between what the technology delivers and what "runs a formally verified kernel" sounds like in a press release is large enough to drive a Jeep through.

What the proof actually says

seL4 is a microkernel developed by the Trustworthy Systems group, originally at NICTA and now at UNSW Sydney. It is roughly ten thousand lines of C, and it has a machine-checked mathematical proof that the implementation conforms to its specification — extended, on some architectures, all the way down to the compiled binary, which removes the C compiler from the set of things you have to trust.

For security purposes the proofs that matter are integrity and confidentiality. Informally: a component running on seL4 cannot modify data it holds no capability to write, and cannot learn information it holds no capability to read. Not "we tested this and it held." Not "we hardened it and hired a red team." It cannot, as a theorem, provided the stated assumptions hold.

That last clause is doing real work and we'll come back to it. But first, why this matters for cars.

Containment, not prevention

Nobody is claiming a microkernel stops your head unit from being hacked. The head unit runs a browser, a Bluetooth stack, a media parser, a cellular modem interface and an app framework. It is going to have vulnerabilities. The claim is narrower and more useful: when it is compromised, the attacker is stuck there.

DARPA's HACMS program produced the clean demonstration. Researchers retrofitted seL4-based software onto a Boeing Unmanned Little Bird helicopter, then gave a red team root access on a non-critical partition and told them to go. They could not reach the flight controls. The isolation held, and the reason it held was not that the team was clever about hardening — it was that the compromised partition simply did not possess the capabilities required to touch the flight control domain, and that fact was proven rather than hoped.

Applied to a vehicle, the architecture looks roughly like this:

This is not hypothetical. The Chinese EV maker NIO ships SkyOS-M, built on seL4, in the mass-produced ONVO L60. NIO is a Premium Member of the seL4 Foundation with a seat on its board, and their engineers presented the production story at the 2024 seL4 Summit. Whatever else you think about this approach, someone is now betting a car company on it.

Where the risk actually goes

Look at that diagram again, specifically the middle box.

The kernel enforces the policy you configured. It does not evaluate whether your policy is any good. And you are going to configure channels between those domains, because the driver wants to see tyre pressure on the touchscreen, adjust the cabin temperature from a phone app, and have the navigation system know how much charge is left. Real vehicles need infotainment and vehicle control to exchange data.

The moment that channel exists, an attack path exists along it. Your actual security now rests on the correctness of a filtering or gateway component that is ordinary, unverified application code, written by ordinary engineers under ordinary deadlines.

This is still a very large improvement. You have taken a system where the attack surface between domains was "twenty million lines of kernel and driver code" and reduced it to "one component whose entire job is to be small and auditable." That is precisely the trade a security architect wants to make. But it is a relocation of risk, not an elimination of it, and the marketing tends to skip that step.

The assumptions attached to the proof

The seL4 team documents these openly, which is to their credit, but several of them bite hard in an automotive context.

Direct memory access. The proofs assume DMA is either disabled or restricted to trusted drivers that you verify yourself. A car is full of DMA-capable peripherals. Handling this correctly means configuring the IOMMU/SMMU properly, and getting it wrong voids the guarantee silently — nothing fails loudly to tell you the theorem no longer applies.

Multicore. This is the sharpest limitation. seL4's proofs model sequential execution. Verification for multicore platforms remains an open problem; Trustworthy Systems have stated they now understand how to do it but lack the funding. An SMP configuration exists and people use it, but it is unverified, and defects have in fact been found in unverified configurations of the kernel including SMP. Automotive SoCs are multicore. The available workaround is a multikernel arrangement with one verified instance per core and hardware strictly partitioned between them, which still does not give whole-system guarantees, because those instances have to trust each other not to corrupt one another's data structures.

Timing channels. The confidentiality proof covers storage channels through architected state the kernel knows about. It explicitly does not address timing channels. Spectre-class microarchitectural leakage is out of scope. There is serious research underway on "time protection" as a principled answer, but the mechanisms so far work in restricted cases on cooperative hardware, and contemporary hardware is largely deficient for the purpose.

Everything underneath. Correctness of the boot code, of the assembly for kernel entry and exit, of TLB and cache-flush operations, and of the hardware behaving as specified. Also, in a real vehicle: the cellular modem's own firmware, any TrustZone secure-world code, and the supply chain that produced all of it.

Platform coverage. The full proof chain, including binary-level correctness, exists for specific architectures and configurations. If the SoC your vehicle programme selected is not among them, you get the architecture and the design discipline without the theorem.

None of these make seL4 a bad choice. They mean the honest claim is "verified under stated assumptions on supported configurations," and that anyone evaluating a vendor should ask which configuration is actually shipping.

What a microkernel does not touch at all

A separate category, and one that microkernel enthusiasm tends to obscure entirely.

The CAN bus is unauthenticated broadcast by design. It was specified in the 1980s for a closed system where every participant was trusted by construction. Any node that can transmit can impersonate any other node. If an attacker lands anywhere with legitimate CAN transmit rights — and something has to have them — isolation upstream does not help. The fixes here are message authentication such as AUTOSAR SecOC, zonal architectures, segmented networks, and moving to authenticated automotive Ethernet. None of these are kernel problems.

Equally untouched: signing and verification of over-the-air updates, key management and storage, physical access through the OBD-II port, relay attacks against keyless entry, and the security of the application code running inside each partition. A verified kernel does nothing for any of it.

So, is it worth it?

Yes, and it should probably be the default for new vehicle architectures. But the operative word is foundation.

What you get is a floor you can reason about mathematically instead of empirically. In security that is genuinely rare. Every other layer of the stack is defended by testing, review, and the accumulated judgment of people who have seen this go wrong before — all valuable, none of it capable of telling you that a class of attack is impossible rather than merely unobserved. seL4 shifts the burden of assurance from twenty million lines of code to roughly ten thousand, plus your inter-domain policy, plus a documented list of assumptions you can go and check.

What you do not get is a secure car. A vehicle built on seL4 with a sloppy gateway component, unauthenticated CAN traffic, and unsigned firmware updates will still be compromised. It will just take slightly longer, and the write-up will be more interesting.

The seL4 project itself is unusually straight about this. Their own FAQ, asked whether the kernel is bug-free, answers that in the formal sense yes, modulo the proof assumptions, and in the ordinary user's sense potentially, because hardware bugs or unmet assumptions may remain — and that the security properties may or may not be sufficient for what your system needs. That is exactly the right register, and it is a useful benchmark for evaluating anyone else who tells you their product is formally verified.

---

Further reading: the seL4 verification status and proof assumptions are documented at sel4.systems. Miller and Valasek's "Remote Exploitation of an Unaltered Passenger Vehicle" (2015) is the Jeep write-up. Klein et al., "seL4: Formal verification of an OS kernel" (SOSP 2009) is the original proof paper.