L4Linux – Linux running on the L4 microkernel
l4linux.org
l4linux.org
> Compared to monolithic Linux, there is a small performance tradeoff because of the µ-kernel architecture. However, the initial L4Linux has been somewhat optimized, and on L4/x86 it has a very acceptable slowdown of less than 4 % for any relevant load.
If it provided any additional security guarantees in trade for that 4%, I imagine it'll become a popular way of running Linux
That being said, last time I checked even sel4 wasn't really hardened against Spectre attacks.
By contrast seL4 is effectively bug free. (Literally bug free for the most the part, but AFAIU some gritty details like TLB management remain outside the scope of the formal verification.) That means you can build a reliable security model for your own application. The guarantees that model can make about confidentiality may be weaker because of Spectre, but you're still in an infinitely better position than on Linux, Windows, or most anywhere else.
seL4 is arguably even better than ARM's TrustZone. With TrustZone you're still stuck having to ensure you correctly manage transitions into and out of protected mode. Bugs in such code constitute a good chunk of kernel vulnerabilities more generally, so it's clearly not trivial. Doing this correctly is basically what seL4 is all about. Then consider the fact that people are trying to push so many tasks into the TrustZone (or secure enclaves in general) that it's common to run an OS in the TrustZone. People would do much better to run seL4 inside the enclaves than bug ridden TEE environments. And unless the enclave is a discrete processor rather than a protected mode as with TrustZone, you may as well just run seL4 as the only OS (or at least the host OS).
Interestingly, Apple's T1 and T2 chips run an L4-based microkernel. AFAIU it's something of a cousin to seL4 but predates it. If seL4 was as mature then as it is now perhaps Apple would have started with seL4.
I mean, yeah, that's what I'm saying. There's some benefit to to running stuff on the side of the kernel, but you gain nothing by running your Linux processes on L4Linux.
> By contrast seL4 is effectively bug free. (Literally bug free for the most the part, but AFAIU some gritty details like TLB management remain outside the scope of the formal verification.) That means you can build a reliable security model for your own application. The guarantees that model can make about confidentiality may be weaker because of Spectre, but you're still in an infinitely better position than on Linux, Windows, or most anywhere else.
The sel4 guys are super careful not to make such strong statements. And it's weird that you'd minimize the consequences of reading out arbitrary memory.
> seL4 is arguably even better than ARM's TrustZone. With TrustZone you're still stuck having to ensure you correctly manage transitions into and out of protected mode. Bugs in such code constitute a good chunk of kernel vulnerabilities more generally, so it's clearly not trivial. Doing this correctly is basically what seL4 is all about. Then consider the fact that people are trying to push so many tasks into the TrustZone (or secure enclaves in general) that it's common to run an OS in the TrustZone. People would do much better to run seL4 inside the enclaves than bug ridden TEE environments. And unless the enclave is a discrete processor rather than a protected mode as with TrustZone, you may as well just run seL4 as the only OS (or at least the host OS).
TrustZone and a microkernel sel4 are totally orthogonal concepts. Your contrasting the two concepts doesn't really make sense. And you can absolutely run sel4 in Secure EL1, you just wouldn't want to run it in EL3 because it's a little heavyweight in its current incarnation for that (hence the guy below talking about how it cut their perf in half).
> Interestingly, Apple's T1 and T2 chips also runs an L4-based microkernel. AFAIU it's something of a cousin to seL4 but predates it. If seL4 was as mature then as it is now perhaps Apple would have started with it.
It's an extremely modified L4:Pistachio that has AFAIK nothing to do with sel4.
"Beware of bugs in the above code; I have only proved it correct, not tried it." -- Donald Knuth on the van Emde Boas construction of priority deques (1977)
I worked with l4 and we had to throw it out because the microcernel overhead had a 2x performance hit on frames per second for animations on a 400mhz arm9.
Are you going to see a 2x hit for disk IOps, or network packets per second, or IO latency?
Were you sending individual graphics commands and rasters over IPC or something, or was that just the cost of the flips, and maybe a second flip from a compositor (or blitter)?
The problem was two fold. L4 ipc was just slower then a swi, and l4 driver model would lock the page table for every region instead of just checking every region all at once.
L4 was just pushed as the “hotness”, and ironically as a way to get around the linux GPL issues at the time.
I don’t want to sound to critical. L4 is actually easier to build drivers for than Linux, and you are much less likely to shoot yourself in the foot.
It’s a great microckernel. It’s just that 4% may all come from the most human sensitive application.
It did. This was the precursor to hypervisors and the first example of virtualization with low overhead, which is now everywhere.
Undoubtably still want propellor controls + stabalization on dedicated hardware, but everything else.
What I mean by this is, run the Linux kernel on L4, then in Linux remove different components by calling out to a library (like virtio does) which actually puts a message onto the L4 bus and has that service handle the request. For example, running an FS as an L4 service.
Not sure if this is possible, but it seems like it should be.
L4, unlike QNX, is so minimal that you have to put another OS on top of it to do much. L4-Linux has been around almost since L4. There's not much point in it unless you have something else running on the same hardware which needs to be isolated. If all you have is one Linux instance, you haven't gained anything.
Putting some container system on top of L4 might be useful.
Disclaimer: not working for them, but used to work on the university project.
I am not very familiar with OS designs and skimming through the landing page didn't help.
Is it essentially a Linux kernel that runs within an existing instance of Linux? Why is it important/useful?
Thanks.
In short, with this project you can run a User Space Linux along with your other user space programs in L4 kernels.
If you want to see a neat demo of this stuff - check out the DROPs demo or TUD:OS http://demo.tudos.org/.
Screenshots of a whole bunch of linuxes (linii?) running at once: http://demo.tudos.org/l4lx_screenshot.png
I think this is from 2003...
Linuces.
The communication overhead remained a problem for microkernels, despite L4's achievements in that area. The advantages were somewhat overstated. The complexity merely moved from the kernel into the applications. A security bug in the IP driver daemon can still compromise the whole system, just like a driver in a monolithic kernel.
Could you speak to how well everything works?
It's not the research project's fault that a different mechanism is used in the public cloud.
As for microkernels, they are actually used, but not in mainstream server systems.