8 ms·

L4Linux – Linux running on the L4 microkernel

140 points by phoe-krk 8y ago

elcritch 8y ago
Anyone used this before? If it supports arm it could be a handy system.
- monocasa 8y ago
  It does support arm, it's one of the primary ways to use sel4.
  - elcritch 8y ago
    Does that mean you could run l4linux with sel4? Didn’t realize the l4 api is consistent/broad enough to do that. That’s cool! The linked “drops” rtos seemed to be dead a long time back.
    - __bjoernd 8y ago
      Not quite. It was rebranded and even is commercially supported these days: https://www.kernkonzept.com/l4re.html https://www.kernkonzept.com/l4re.html
    - vertex-four 8y ago
      There is no documentation that I can find regarding Linux running on seL4, outside of hardware virtualisation.
- yjftsjthsd-h 8y ago
  Can I ask what you'll find it useful for? The technology is neat, I'm just struggling to think of something that would benefit from it.
  - elcritch 8y ago
    Primarily for soft (or hard) real time operations. Even kernel modules running in a RT-Linux have a difficult time responding consistently to an IRQ at sub-10 uS latency. Of course, the larger SoC capable of running Linux can have hardware latencies due to shared data buses, etc. but still having a RTOS layer “underneath” Linux would be a good way to ensure more consistent responses.
Firerouge 8y ago
This 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
- monocasa 8y ago
  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.
  - wahern 8y ago
    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.
Koshkin 8y ago
The idea seems to be to use paravirtualized Linux as a “time-sharing component” of a system that otherwise provides real-time capabilities...
- nixpulvis 8y ago
  This might be interesting for my long abandoned drone project... Undoubtably still want propellor controls + stabalization on dedicated hardware, but everything else.
vicnov 8y ago
Okay, 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.
- omeid2 8y ago
  L4 is a family of microkernels with a namesake kernel interface. μ-kernel (minix3, L4/Fiasco et al) are extremely lean by design and unlike monolithic (Linux, Solaris, Darwin et al), leave device drivers, filesystem, and a lot of non-hardware related stuff to the userspace. This project is basically a port of linux to an L4 Hypervisor that can Para-Virtualize Linux. In short, with this project you can run a User Space Linux along with your other user space programs in L4 kernels.
- butterisgood 8y ago
  Microkernels and hypervisors are very closely related in the view of some. Paravirtualization, like L4 Linux, is when the guest is aware of being hosted and, at one time - maybe still, could outperform guest OSes on fully virtualized hardware. I'm not sure if that's all still true since Intel and AMD implemented VTX. If you want to see a neat demo of this stuff - check out the DROPs demo or TUD:OS http://demo.tudos.org/ http://demo.tudos.org/. Screenshots of a whole bunch of linuxes (linii?) running at once: http://demo.tudos.org/l4lx_screenshot.png http://demo.tudos.org/l4lx_screenshot.png I think this is from 2003...
  - Koshkin 8y ago
    > linii? Linuces.
- bewo001 8y ago
  The idea was to have something you would call microservice architecture today, just for OS functions. An ethernet driver server application would talk to an IP server, which would talk to a TCP server that distributes messages to the applications. The kernel would just isolate all those applications and enable communication between them. If the ethernet driver daemon crashed you would just restart it. 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.
bluejekyll 8y ago
I’ll ask a naive question. Could L4 in this context be used as a means to migrate Linux to a micro-kernel architecture? 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.
- Animats 8y ago
  Unfortunately, no. 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.
newnewpdro 8y ago
Does anyone here have experience running this on desktop/laptop for general use? Does GPU acceleration in opengl/vulkan work? Intel integrated HD audio? Could you speak to how well everything works?
andrewflnr 8y ago
Can you use this setup to use Linux's device drivers for SeL4? Given the paranoia level involved, I imagine you'd run a stripped down Linux kernel per driver, with all device commands proxied through L4. Your Linux or whatever other userland would see virtual devices through L4 as well. Possible? Hopelessly inefficient? Or does L4's capability pipelining save the day?
- jakeogh 8y ago
  there's this for NetBSD's drivers: https://research.csiro.au/tsblog/using-rump-kernels-to-run-unmodified-netbsd-drivers-on-sel4/ https://research.csiro.au/tsblog/using-rump-kernels-to-run-u...
__bjoernd 8y ago
Might be worth noting that this link itself points to the university project. Most of the main developers moved on and founded a company that's providing microkernel technology commercially: https://www.kernkonzept.com https://www.kernkonzept.com Disclaimer: not working for them, but used to work on the university project.
butterisgood 8y ago
This is at least a decade old... If it was going to become a popular way of running Linux, as some have suggested, what's stopped it so far?
- __bjoernd 8y ago
  Virtual machines running Linux have actually become quite popular in the past decade. ;) 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.
MR4D 8y ago
Might be a nice alternative to Docker.

140 points by phoe-krk 8y ago

elcritch 8y ago

Anyone used this before? If it supports arm it could be a handy system.

monocasa 8y ago
It does support arm, it's one of the primary ways to use sel4.
- elcritch 8y ago
  Does that mean you could run l4linux with sel4? Didn’t realize the l4 api is consistent/broad enough to do that. That’s cool! The linked “drops” rtos seemed to be dead a long time back.
  - __bjoernd 8y ago
    Not quite. It was rebranded and even is commercially supported these days: https://www.kernkonzept.com/l4re.html https://www.kernkonzept.com/l4re.html
  - vertex-four 8y ago
    There is no documentation that I can find regarding Linux running on seL4, outside of hardware virtualisation.
yjftsjthsd-h 8y ago
Can I ask what you'll find it useful for? The technology is neat, I'm just struggling to think of something that would benefit from it.
- elcritch 8y ago
  Primarily for soft (or hard) real time operations. Even kernel modules running in a RT-Linux have a difficult time responding consistently to an IRQ at sub-10 uS latency. Of course, the larger SoC capable of running Linux can have hardware latencies due to shared data buses, etc. but still having a RTOS layer “underneath” Linux would be a good way to ensure more consistent responses.

Firerouge 8y ago

This 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

monocasa 8y ago
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.
- wahern 8y ago
  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.

Koshkin 8y ago

The idea seems to be to use paravirtualized Linux as a “time-sharing component” of a system that otherwise provides real-time capabilities...

nixpulvis 8y ago
This might be interesting for my long abandoned drone project... Undoubtably still want propellor controls + stabalization on dedicated hardware, but everything else.

vicnov 8y ago

Okay, 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.

omeid2 8y ago
L4 is a family of microkernels with a namesake kernel interface. μ-kernel (minix3, L4/Fiasco et al) are extremely lean by design and unlike monolithic (Linux, Solaris, Darwin et al), leave device drivers, filesystem, and a lot of non-hardware related stuff to the userspace. This project is basically a port of linux to an L4 Hypervisor that can Para-Virtualize Linux. In short, with this project you can run a User Space Linux along with your other user space programs in L4 kernels.
butterisgood 8y ago
Microkernels and hypervisors are very closely related in the view of some. Paravirtualization, like L4 Linux, is when the guest is aware of being hosted and, at one time - maybe still, could outperform guest OSes on fully virtualized hardware. I'm not sure if that's all still true since Intel and AMD implemented VTX. If you want to see a neat demo of this stuff - check out the DROPs demo or TUD:OS http://demo.tudos.org/ http://demo.tudos.org/. Screenshots of a whole bunch of linuxes (linii?) running at once: http://demo.tudos.org/l4lx_screenshot.png http://demo.tudos.org/l4lx_screenshot.png I think this is from 2003...
- Koshkin 8y ago
  > linii? Linuces.
bewo001 8y ago
The idea was to have something you would call microservice architecture today, just for OS functions. An ethernet driver server application would talk to an IP server, which would talk to a TCP server that distributes messages to the applications. The kernel would just isolate all those applications and enable communication between them. If the ethernet driver daemon crashed you would just restart it. 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.

bluejekyll 8y ago

I’ll ask a naive question. Could L4 in this context be used as a means to migrate Linux to a micro-kernel architecture? 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.

Animats 8y ago
Unfortunately, no. 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.

newnewpdro 8y ago

Does anyone here have experience running this on desktop/laptop for general use? Does GPU acceleration in opengl/vulkan work? Intel integrated HD audio? Could you speak to how well everything works?

andrewflnr 8y ago

Can you use this setup to use Linux's device drivers for SeL4? Given the paranoia level involved, I imagine you'd run a stripped down Linux kernel per driver, with all device commands proxied through L4. Your Linux or whatever other userland would see virtual devices through L4 as well. Possible? Hopelessly inefficient? Or does L4's capability pipelining save the day?

jakeogh 8y ago
there's this for NetBSD's drivers: https://research.csiro.au/tsblog/using-rump-kernels-to-run-unmodified-netbsd-drivers-on-sel4/ https://research.csiro.au/tsblog/using-rump-kernels-to-run-u...

__bjoernd 8y ago

Might be worth noting that this link itself points to the university project. Most of the main developers moved on and founded a company that's providing microkernel technology commercially: https://www.kernkonzept.com https://www.kernkonzept.com Disclaimer: not working for them, but used to work on the university project.

butterisgood 8y ago

This is at least a decade old... If it was going to become a popular way of running Linux, as some have suggested, what's stopped it so far?

__bjoernd 8y ago
Virtual machines running Linux have actually become quite popular in the past decade. ;) 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.

MR4D 8y ago

Might be a nice alternative to Docker.