HACKER Q&A
📣 AlexWandell

What runs L4-related microkernels/hypervisors these days?


I've been learning about the L4 microkernel, and am thinking about doing something related to it for a research project. I'm especially curious about more recent examples of specific devices that run L4 variants (seL4, PikeOS, OKL4, etc.). I already found a few that use seL4, but to take OKL4 as an example, most of the specific devices I could find are from more than a decade ago, and I'm trying to find things from at least the last 5 or 6 years. I'm even more curious to find devices that use a form of L4 as a hypervisor.

Has anyone here worked on a device that used an L4-related kernel or hypervisor? I know one major area they're used in is defense and full of NDAs, but hopefully some of the other industries they're used in (medical devices, automotive, IoT) are a little less restrictive. Thanks in advance!

  👤 hatsubai Accepted Answer ✓
You're correct that they're used a decent bit in the defense industry. I can't talk too much about it for obvious reasons, but it's an area where I would expect an uptick in their usage within the next decade in the defense field alone. Check out the DoD's modernization efforts regarding seL4 and L4Re. In-depth knowledge of these microkernels is going to be a skillset in very high demand as defense contractors are forced to adhere to the modernization efforts pushed forth by the DoD.
👤 senko
Tangentially, I'd have loved to see a modern, (se)L4 based desktop (general purpose) operating system, capabilities-based, with services written in a safe language, with no legacy (POSIX) baggage.

Failing that, I hope to be able to hack on something along those lines when I retire :)

(before someone mentiones Fuchsia - Zircon is cool'n'all, but we're talking about L4 here)

👤 4suc
https://kernkonzept.com/ is a company developing the L4Re OS. The company is a spinoff from the TU Dresden Operating Systems group. Afaik their main customer is the automotive industry which uses their hypervisor. L4Re is also certified for all kinds of government secrecy levels, so I would assume they have some users in that area.
👤 kev009
I believe Apple uses it in at least one of the auxiliary service processors in their current portfolio under the moniker "Darbat" or "L4/xnu"

https://citeseerx.ist.psu.edu/document?repid=rep1&type=pdf&d...

https://microkerneldude.org/2016/04/14/so-the-fbi-cracked-th...

👤 snvzz
seL4 foundation member list[0] might give you some hints.

0. https://sel4.systems/Foundation/Membership/

👤 saagarjha
Apple’s Secure Enclave Processor?
👤 wrycoder
You could check out Helios, which is inspired by L4 [0]

[0] https://ares-os.org/docs/helios/

👤 dwaite
I believe the Qualcomm modems run a L4 variant.