Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

L4Linux – Linux running on the L4 microkernel

l4linux.org

Post reply on HN
Print view View original

21–30 of 42 posts

Re: L4Linux – Linux running on the L4 microkernel

#21

Post by Animats »

bluejekyll wrote: post #15

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 possibl…

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.

Re: L4Linux – Linux running on the L4 microkernel

#22

Post by sanxiyn »

j16sdiz wrote: post #19
wahern wrote: post #7

Earlier quoted context omitted.

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 effort…

seL4 is bug free in theory, not in paratice. It have been proved to follow the spec, but the spec can have error. Missing workaround for hardware bug can bite too. "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)

After proving the full functional correctness (that machine code implements spec), they did additional security proofs against the spec, including confidentiality and integrity. If you accept their TCB(no hardware bugs etc), the entire proof is incredibly strong.

Re: L4Linux – Linux running on the L4 microkernel

#23

Post by __bjoernd »

elcritch wrote: post #20
monocasa wrote: post #9

Earlier quoted context omitted.

It does support arm, it's one of the primary ways to use sel4.

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.

Not quite. It was rebranded and even is commercially supported these days: https://www.kernkonzept.com/l4re.html

Re: L4Linux – Linux running on the L4 microkernel

#24

Post by __bjoernd »

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

Disclaimer: not working for them, but used to work on the university project.

Re: L4Linux – Linux running on the L4 microkernel

#25

Post by 616c »

monocasa wrote: post #5
Firerouge wrote: post #3

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 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…

That sounds like a very neat CTF. I'll search but do you know if anyone wrote about it or documented it?

Re: L4Linux – Linux running on the L4 microkernel

#26

Post by vertex-four »

elcritch wrote: post #20
monocasa wrote: post #9

Earlier quoted context omitted.

It does support arm, it's one of the primary ways to use sel4.

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.

There is no documentation that I can find regarding Linux running on seL4, outside of hardware virtualisation.

Re: L4Linux – Linux running on the L4 microkernel

#27

Post by rurban »

monocasa wrote: post #5
Firerouge wrote: post #3

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 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…

The Australian sel4 is not yet Spectre fixed, but the Dresden L4Re is.

Re: L4Linux – Linux running on the L4 microkernel

#28

Post by naasking »

Firerouge wrote: post #3

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 runnin…

> If it provided any additional security guarantees in trade for that 4%, I imagine it'll become a popular way of running Linux

It did. This was the precursor to hypervisors and the first example of virtualization with low overhead, which is now everywhere.

Re: L4Linux – Linux running on the L4 microkernel

#29

Post by alalo »

aey wrote: post #6
Firerouge wrote: post #3

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 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?

ARM9's cache architecture is not suited for frequent address space switches due to the requirement to flush caches on every switch. All multi-user OSes suffer there it's just more accentuated on microkernels.
Post reply on HN