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

L4 microkernels: The lessons from 20 years of research and deployment

ts.data61.csiro.au

Post reply on HN
Print view View original

61–70 of 99 posts

Re: L4 microkernels: The lessons from 20 years of research and deployment

#61

Post by Animats »

derefr wrote: post #59
Animats wrote: post #58

The paper doesn't mention QNX at all. QNX is similar to early L4, but they've taken slightly different paths. L4 got rid of "long message passing", in favor of shared memory and interrupt-like IPC. This is great for the kernel - no copying delays and no buffering problems. But it means that communicating processes have to share some memory pages and cooperate properly. If the shared memory page is something like a ch…

How do these compare to Mach IPC in OSX?

Here's a Linux/L4/QNX comparison.[1]

My favorite table:

    Kernel         Source Lines of Code (SLOC)

     OKL4                 13.8k
     QNX Neutrino v6.3.2  23k
     Linux Kernel 2.6.0   5.2M
     Windows XP           Kernel size unknown but totals at approx 40M
     Windows Vista        Kernel size unknown but totals at approx 50M
Modern microkernels are so small that they can be thoroughly debugged, or formally verified.

[1] http://www.gelato.unsw.edu.au/IA64wiki/JamieLennox/QNXvL4?ac...

Re: L4 microkernels: The lessons from 20 years of research and deployment

#62

Post by pslam »

tptacek wrote: post #15
mafribe wrote: post #9

Earlier quoted context omitted.

True, seL4 verification doesn't solve the application level security problem but it makes it more approachable in several ways. - No longer need the verification of application make assumptions about the semantics of the operating system. Instead, concrete and verified semantics are available. This makes application specification and verification easier, and safer. Fortunately, verification is cumulative - The seL4 p…

What's your sense of the number of IoT vulnerabilities that are due to misconstrued OS semantics? Mine --- and I've done a bit of work here, but not that much --- is that there aren't that many. Really I think it depends on what you're doing. If the work you're doing is fundamentally kernel work --- if it's all about interacting with the security boundaries of the hardware (not just "interacting with hardware", like…

The problem is it takes more than just implementing the "kernel" (as in low-level access aka HAL) work under L4. You need to apply that compartmentalization all the way through the stack, and even subdivide applications into smaller chunks of responsibility.

What you typically get is a neat subdivision of all the HAL bits, but everyone stops once they're plugging in applications. This is partly because there's normally a large amount of shared/legacy code which needs importing, and partly because people don't recognize the benefits of partitioning an app.

It's not all bad - at least you can be reasonably confident that one compromised app, or part of the HAL, can't be trivially used to compromise the rest of the system. But, as you say elsewhere here, if there's just one thing you're doing, then all that effort didn't really improve things.

Re: L4 microkernels: The lessons from 20 years of research and deployment

#63

Post by hackuser »

tptacek wrote: post #36
pjmlp wrote: post #27

Earlier quoted context omitted.

If written in languages like C and C++, you just get the own the complete device when exploiting application errors. It can also happen when using unsafe code with the Ada, Java, Pascal and Basic variants available for such devices, but the probability is lower.

Right, but if the device exists more or less to run a single program or small set of programs, what do I care if I own the box once I've taken control of that program?

You could run other programs on the box.

Re: L4 microkernels: The lessons from 20 years of research and deployment

#64

Post by berkeleynerd »

tptacek wrote: post #3
shandor wrote: post #2

I'm having really big expectations on seL4. The modularity of a microkernel with the security of formal methods is something that would give hope of solving some really fundamental problems with the "IoT scene". I.e. having good security out of the box (which is horrible in IoT as of now), while still maintaining good flexibility regarding platforms (which will become more and more of a problem in the future when IoT…

L4 is great, but it doesn't solve application security problems. L4 by itself doesn't do much, and whatever you build on top of it --- if you're not yourself using formal methods, which very few real product teams do --- isn't going to inherit its security.

Is Mirage on L4 something that, if realized, would provide application developers with a more secure basis for building their own applications? I'm but a simple application developer but I do care about security and if there were a platform I could develop against that gave me confidence my code was far less likely to be undermined by kernel or TCP stack vulnerabilities I think I'd be encouraged to do a better job of security myself. This might not be the ideal human attitude toward secure programming but I might not be alone in feeling like my best efforts rest on shaky foundations and that's somewhat demoralizing.

Re: L4 microkernels: The lessons from 20 years of research and deployment

#65

Post by tptacek »

hackuser wrote: post #63
tptacek wrote: post #36

Earlier quoted context omitted.

Right, but if the device exists more or less to run a single program or small set of programs, what do I care if I own the box once I've taken control of that program?

You could run other programs on the box.

Without some kind of formally assured way of building your application, you can do that anyways.

Re: L4 microkernels: The lessons from 20 years of research and deployment

#66

Post by rayiner »

derefr wrote: post #59
Animats wrote: post #58

The paper doesn't mention QNX at all. QNX is similar to early L4, but they've taken slightly different paths. L4 got rid of "long message passing", in favor of shared memory and interrupt-like IPC. This is great for the kernel - no copying delays and no buffering problems. But it means that communicating processes have to share some memory pages and cooperate properly. If the shared memory page is something like a ch…

How do these compare to Mach IPC in OSX?

Note OS X mostly doesn't use Mach IPC for anything. Calling, e.g., write() results in a system call into the BSD portion of the XNU kernel, not all that different from what happens on Linux.

Re: L4 microkernels: The lessons from 20 years of research and deployment

#67

Post by tptacek »

Animats wrote: post #58

The paper doesn't mention QNX at all. QNX is similar to early L4, but they've taken slightly different paths. L4 got rid of "long message passing", in favor of shared memory and interrupt-like IPC. This is great for the kernel - no copying delays and no buffering problems. But it means that communicating processes have to share some memory pages and cooperate properly. If the shared memory page is something like a ch…

L4 can be used that way, but in purpose-built systems it can also just be used as a simple stratum on which to build applications directly. If you were using L4 to build a baseband package, for instance, you probably wouldn't run a full OS on top of it.

My intuition, not carefully checked:

I'd rather be using QNX than Linux on L4, but I'd rather be using just L4 than QNX.

Re: L4 microkernels: The lessons from 20 years of research and deployment

#68

Post by tptacek »

rayiner wrote: post #66
derefr wrote: post #59

Earlier quoted context omitted.

How do these compare to Mach IPC in OSX?

Note OS X mostly doesn't use Mach IPC for anything. Calling, e.g., write() results in a system call into the BSD portion of the XNU kernel, not all that different from what happens on Linux.

OS X doesn't use Mach IPC to emulate POSIX, but it uses (or did last I checked, which was a while ago) Mach IPC directly for things like launchd.

Re: L4 microkernels: The lessons from 20 years of research and deployment

#69

Post by [deleted] »

rayiner wrote: post #66
derefr wrote: post #59

Earlier quoted context omitted.

How do these compare to Mach IPC in OSX?

Note OS X mostly doesn't use Mach IPC for anything. Calling, e.g., write() results in a system call into the BSD portion of the XNU kernel, not all that different from what happens on Linux.

[deleted]

Re: L4 microkernels: The lessons from 20 years of research and deployment

#70

Post by cvwright »

Animats wrote: post #58

The paper doesn't mention QNX at all. QNX is similar to early L4, but they've taken slightly different paths. L4 got rid of "long message passing", in favor of shared memory and interrupt-like IPC. This is great for the kernel - no copying delays and no buffering problems. But it means that communicating processes have to share some memory pages and cooperate properly. If the shared memory page is something like a ch…

There are efforts to build OSes directly on L4 kernels as well. Most notably Genode. http://genode.org/

They recently added support for running on seL4 too: https://sel4.systems/pipermail/devel/2016-August/000967.html

Post reply on HN