6 ms·

Ask HN: What runs L4-related microkernels/hypervisors these days?

115 points by AlexWandell 2y ago

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!

saagarjha 2y ago
Apple’s Secure Enclave Processor?
- rgovostes 2y ago
  Citation: https://support.apple.com/en-gb/guide/security/sec59b0b31ff/web https://support.apple.com/en-gb/guide/security/sec59b0b31ff/... "The Secure Enclave Processor runs an Apple-customised version of the L4 microkernel." From the rumor mill morgue, back in 2006 there was some speculation about macOS, err, Mac OS X transitioning to L4: https://arstechnica.com/staff/2006/06/4407/ https://arstechnica.com/staff/2006/06/4407/
  - gaze 2y ago
    They hired a ton of UNSW graduates who had worked on L4 around that time.
    - isubasinghe 2y ago
      Was at UNSW recently, can confirm that apple doing special L4 stuff right now.
- AlexWandell 2y ago
  Nice! Yeah, that's definitely modern enough. Do you know if it runs as a hypervisor in the Secure Enclave firmware? It seems like the processor itself is low-power enough that it might not have virtualization features.
  - mech422 2y ago
    This(1)(2) any good for ya? "Genode's microkernel architecture, capability-based security, sandboxed device drivers, and virtual machines in a novel operating system for commodity PC hardware and the PinePhone. Sculpt is used as day-to-day OS by the Genode developers. " 1) https://genode.org/ https://genode.org/ 2) https://genode.org/download/sculpt https://genode.org/download/sculpt
  - saagarjha 2y ago
    I am pretty sure there is no hypervisor. I am pretty sure the processor supports EL2 but it doesn't get used for anything to my knowledge.
dwaite 2y ago
I believe the Qualcomm modems run a L4 variant.
- AlexWandell 2y ago
  I know that at one point they did (2012-ish), but do they still? From what I could make of some of the recent reverse engineering research on Qualcomm modems, they seem to suggest that they've been using a homegrown RTOS for awhile now.
senko 2y ago
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)
- throwawaymaths 2y ago
  Safe what? Rust isn't memory safe if you are using unsafe anywhere. There are other "safety" issues with rust as well. Sel4 is in c but it's provably safe (if you're on arm).
  - junon 2y ago
    This comment demonstrates a lack of understanding of what the unsafe keyword is for in Rust. Unsafe specifically states that no code within it may introduce UB after the unsafe block exits (post-condition). It also doesn't allow certain operations no matter how hard you try (e.g. the borrow checker still applies, but you can use raw pointers in ways you couldn't outside of an unsafe block, assuming you don't introduce UB). As someone designing a kernel in Rust, you literally cannot avoid unsafe code, regardless of the language, to implement a kernel. It's worth mentioning that "unsafe" and "vulnerable" are two different things. SeL4 is safe because of its extensively verified codebase written in a language suited for verification. Last I checked they port it to C after the fact, but it could just as well be ported to Rust. It'd still be "unsafe" but significantly less "vulnerable". For example, modifying cr3 or TTBRn_EL1 is incredibly unsafe. But it happens all the time when context switching. In the kernel I use `unsafe` pretty commonly to denote functions with preconditions not representable by the type system. This enforcement wouldn't even be possible in C or any other language I know of personally that'd be efficient to write an OS in. The only gripe I have with Rust's unsafe is that I can't mark methods with preconditions as unsafe while still requiring `unsafe` clauses within the function body. I've thought about opening an RFC for `unsafe(pub)` for this reason. But doing so has made iteration and overall safety of the codebase much easier to reason about because it forces me to think about every call site in which I might introduce a problem if not done carefully.
snvzz 2y ago
seL4 foundation member list[0] might give you some hints. 0. https://sel4.systems/Foundation/Membership/ https://sel4.systems/Foundation/Membership/
4suc 2y ago
https://kernkonzept.com/ 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.
- dloss 2y ago
  Two products for one-way data transfer, based on L4Re: - https://www.genua.eu/it-security-solutions/data-diode-cyber-diode https://www.genua.eu/it-security-solutions/data-diode-cyber-... - https://www.genua.eu/it-security-solutions/data-diode-vs-diode https://www.genua.eu/it-security-solutions/data-diode-vs-dio... Disclaimer: I work for genua, the maker of these products.
- usr1106 2y ago
  They used to be involved in the "chancellor phone", a hypervised system with an open Android OS and a more closed side. It's 10 years ago. I have no idea whether the product still exists and if yes, if it's still done the same way.
kev009 2y ago
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&doi=e148cceb117c5cce63e933f6ad552f17daf74d28 https://citeseerx.ist.psu.edu/document?repid=rep1&type=pdf&d... https://microkerneldude.org/2016/04/14/so-the-fbi-cracked-the-iphone-with-a-zero-day-and-hardware/ https://microkerneldude.org/2016/04/14/so-the-fbi-cracked-th...
- atombender 2y ago
  Darbat was their project mainly to run macOS on L4. AFAIK this was canceled, and no work has happened since around 2006. The newer L4 stuff (like Apple's Secure Enclave) is based on L4Ka::Pistachio, but with proprietary changes made by Apple. [1] [1] https://www.blackhat.com/docs/us-16/materials/us-16-Mandt-Demystifying-The-Secure-Enclave-Processor.pdf https://www.blackhat.com/docs/us-16/materials/us-16-Mandt-De...
wrycoder 2y ago
You could check out Helios, which is inspired by L4 [0] [0] https://ares-os.org/docs/helios/ https://ares-os.org/docs/helios/
hatsubai 2y ago
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.

andreww591 2y ago

It's not completely "legacy-free", nor is it purely capability-oriented, but I'm writing a QNX-like OS (https://gitlab.com/uxrt/uxrt-toplevel https://gitlab.com/uxrt/uxrt-toplevel) based on a kernel forked from seL4 with a preference for servers written in safer languages. Even though it is going to be fairly Unix-like it will diverge from conventional Unix in a number of ways and either discard or demote quite a few legacy Unix features. For example, there will be no support for reversion to the traditional Unix security model in the core OS, with the base VFS implementing a security model based on a mix of per-process ACLs and capability transfers, and on top of that there will be a role-based access control model (there will be a fakeroot-type compatibility layer that simulates traditional Unix security within an environment constrained by the native security model). I don't think there's a good way to make a purely capability-oriented general-purpose OS since as soon as you have a way to look up files by human-readable names instead of capabilities your OS is no longer purely capability-oriented. IMO most of the issues with typical Unix-like OSes are more due to specific outdated architectural features rather than the Unix API or shell environment. A lot of what could be done with a completely new OS could instead be done by designing a Unix-like OS for extensibility by reducing the core API down to a small set of file calls that act as an IPC transport layer and name service and then building everything on top of that, building object-oriented wrapper libraries on top of the filesystem, and reimplementing the traditional Unix APIs outside the core filesystem ones on top of the newer APIs. Existing applications could be ported to such a system incrementally rather than having to do everything all at once or relegate them to some kind of limited "penalty box" compatibility layer (and any binary compatibility layer for Linux or other conventional Unices would integrate better into such a system than into something completely new).