L4 microkernels: The lessons from 20 years of research and deployment • Hacker News Board

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

#81

Post by [deleted] » Wed, Sep 21, 2016, 5:20 AM UTC

_cbsz wrote: post #77

rayiner wrote: post #75

Earlier quoted context omitted.

Yes, I'd assume it's more heavily used in the higher-level application layer. I was talking about basic UNIX functions.

Even Unix signals are delivered as Mach exceptions first. If the process doesn't have a Mach exception handler set up, the kernel's exception handler converts them to Unix signals and tries delivery that way: https://github.com/opensource-apple/xnu/blob/27ffc00f33925b5... and https://github.com/opensource-apple/xnu/blob/27ffc00f33925b5...

[deleted]

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

#82

Post by harry8 » Wed, Sep 21, 2016, 6:42 AM UTC

This is a republish of an old paper which was pure, uncritical review of the authors' triumphs.

Look for the part where they identify their responsibility for the fact that after 20 years and thousands of engineer hours at their disposal they still don't have a microkerenel based operating system worth a pinch of anything. I'm not trolling, I'd love it if that statement were false.

"For a successful technology, reality must take precedence over public relations, for Nature cannot be fooled." --Richard Feynman

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

#83

Post by pjmlp » Wed, Sep 21, 2016, 6:57 AM UTC

cmrx64 wrote: post #31

pjmlp wrote: post #28

Earlier quoted context omitted.

Not really, to verify C code you need to set the compiler and its corresponding version in stone for the verification process, as UB can change even between versions of the same compiler.

Not really true. See https://www.nicta.com.au/publications/research-publications/... for how the compiler and its internal semantics are completely removed from the chain for l4v.

Thanks for the link, I will have a look into it.

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

#84

Post by pjmlp » Wed, Sep 21, 2016, 7:02 AM UTC

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?

True, but by having everything on the same memory space, unless a memory safe language is being used, it means the amount of possible exploits is much higher, thus leading to an higher probability of owning the device.

The isolation helps reducing the attack surface.

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

#85

Post by pjmlp » Wed, Sep 21, 2016, 7:36 AM UTC

ori_b wrote: post #80

Animats wrote: post #61

Earlier quoted context omitted.

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

On a related note, QNX was open source for a while, before it was bought by Blackberry. Do you know if anyone managed to snag a copy of it?

It was available for free on a floppy, but never open source.

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

#86

Post by faragon » Wed, Sep 21, 2016, 8:10 AM UTC

In my opinion, the lesson is that microkernels are too small (e.g. lacking per-user/group security schemes), and monolithic kernels are too big.

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

#87

Post by pawadu » Wed, Sep 21, 2016, 8:15 AM UTC

Animats wrote: post #61

derefr wrote: post #59

Earlier quoted context omitted.

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

Kind of off-topic, but where can I find the OKL4 source code?

All I have found is a really old version that doesn't seem to have much in common with the current one.

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

#88

Post by bicolao » Wed, Sep 21, 2016, 9:31 AM UTC

pawadu wrote: post #87

Animats wrote: post #61

Earlier quoted context omitted.

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

Kind of off-topic, but where can I find the OKL4 source code? All I have found is a really old version that doesn't seem to have much in common with the current one.

This is from 2015, not sure if it's that old.

https://github.com/tomga/genode/commit/c8a64b5c3465cde1723b2...

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

#89

Post by pawadu » Wed, Sep 21, 2016, 10:03 AM UTC

bicolao wrote: post #88

pawadu wrote: post #87

Earlier quoted context omitted.

Kind of off-topic, but where can I find the OKL4 source code? All I have found is a really old version that doesn't seem to have much in common with the current one.

This is from 2015, not sure if it's that old. https://github.com/tomga/genode/commit/c8a64b5c3465cde1723b2...

I think the latest version is 5 or 6. The one you pointed to seems to be pretty old:

    OKL4 Release 2.1
    ================
    
    Date: 15 April 2008

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

#90

Post by wolfgke » Wed, Sep 21, 2016, 1:36 PM UTC

pjmlp wrote: post #85

ori_b wrote: post #80

Earlier quoted context omitted.

On a related note, QNX was open source for a while, before it was bought by Blackberry. Do you know if anyone managed to snag a copy of it?

It was available for free on a floppy, but never open source.

It was never open source in the sense of the OSI (Open Source Initiative) definition, but the source code was available to the public for a while:

> https://en.wikipedia.org/w/index.php?title=QNX&oldid=7308275...

"In September 2007, QNX Software Systems announced the availability of some of its source code. [http://www.qnx.com/news/pr_2471_1.html]

On April 9, 2010, Research In Motion announced they would acquire QNX Software Systems from Harman International Industries. On the same day, QNX source code access was restricted from the public and hobbyists."