L4Linux – Linux running on the L4 microkernel
1–10 of 42 posts
Re: L4Linux – Linux running on the L4 microkernel
#2Anyone used this before? If it supports arm it could be a handy system.
Re: L4Linux – Linux running on the L4 microkernel
#3This seems like an important part that's buried
> 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
Re: L4Linux – Linux running on the L4 microkernel
#4The idea seems to be to use paravirtualized Linux as a “time-sharing component” of a system that otherwise provides real-time capabilities...
Re: L4Linux – Linux running on the L4 microkernel
#5This seems like an important part that's buried > 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 runnin…
It doesn't really provide extra security for processes managed by the Linux kernel, but it allows you to co locate Linux and some other code. I could see a model where you have an untrusted Linux land running next to some unikernel like rtos-esque components that are protected from the Linux side. The sel4 guys had a CTF where they ran hard realtime heleicopter software next to a Linux kernel on the same system, and gave you a root shell to the Linux side to start off with.
That being said, last time I checked even sel4 wasn't really hardened against Spectre attacks.
Re: L4Linux – Linux running on the L4 microkernel
#6This seems like an important part that's buried > 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 runnin…
4% is meaningless measurement for an OS kernel.
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?
Re: L4Linux – Linux running on the L4 microkernel
#7This seems like an important part that's buried > 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 runnin…
It doesn't really provide extra security for processes managed by the Linux kernel, but it allows you to co locate Linux and some other code. I could see a model where you have an untrusted Linux land running next to some unikernel like rtos-esque components that are protected from the Linux side. The sel4 guys had a CTF where they ran hard realtime heleicopter software next to a Linux kernel on the same system, and…
By exposing kernel memory Spectre diminishes the effectiveness of mitigations like kernel ASLR as well as makes it easier more generally to exploit kernel vulnerabilities. That's significant in the case of Linux as there's no shortage of Linux kernel bugs, not now nor for the foreseeable future. Even well written, bug free user space applications can't protect themselves from the kernel, AMD's and Intel's best efforts with SEV and SGX, respectively, notwithstanding.
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.
Re: L4Linux – Linux running on the L4 microkernel
#8The idea seems to be to use paravirtualized Linux as a “time-sharing component” of a system that otherwise provides real-time capabilities...
This might be interesting for my long abandoned drone project...
Undoubtably still want propellor controls + stabalization on dedicated hardware, but everything else.
Re: L4Linux – Linux running on the L4 microkernel
#9Anyone used this before? If it supports arm it could be a handy system.
It does support arm, it's one of the primary ways to use sel4.
Re: L4Linux – Linux running on the L4 microkernel
#10Okay, can someone explain why is this a thing? It is a genuine question.
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.