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

91–99 of 99 posts

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

#91

Post by Animats »

wolfgke wrote: post #90
pjmlp wrote: post #85

Earlier quoted context omitted.

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

Yes, and much of the QNX development community abandoned QNX when they did that.

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

#92

Post by kragen »

harry8 wrote: post #82

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

In 2011, supposedly L4 passed a billion installs, including being the basis for the iPad 2, the Motorola Evoke, and some Qualcomm phones: https://stackoverflow.com/questions/8405505/is-there-any-app...

I don't have personal knowledge of these environments, so I wouldn't know if I were wrong about this.

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

#93

Post by indolering »

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…

I would really love to see more commentary from high-level systems people on how suitable SEL4 is as the basis for a general purpose OS. It seems like it's security guarantees would be driving a lot more outside investment than it has received.

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

#94

Post by indolering »

nickpsecurity wrote: post #78
indolering wrote: post #73

Earlier quoted context omitted.

You wouldn't, SEL4 isn't designed for embedded systems. That's what NICTA's eChronos [1] is for : ) 1: http://ts.data61.csiro.au/projects/TS/echronos/

seL4 is designed for embeddee systems. That's why it mainly targeted ARM. Gernot Heiser even said so. I believe eChronos is just targeted for embedded devices with more constrained hardware.

> I believe eChronos is just targeted for embedded devices with more constrained hardware.

I guess it all depends on which meaning of IoT and embedded you are using.

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

#95

Post by indolering »

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?

What if you can't take control of the program, like Ironsides? It seems as if your premise is that it's too complex to verify the application layer. However, you don't need to model every behavior in a program and this can be leveraged to reduce proofing overhead. A recent paper [1] produced 1: https://pdfs.semanticscholar.org/bc9c/491e215d4abad1be7de944...

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

#96

Post by nickpsecurity »

indolering wrote: post #94
nickpsecurity wrote: post #78

Earlier quoted context omitted.

seL4 is designed for embeddee systems. That's why it mainly targeted ARM. Gernot Heiser even said so. I believe eChronos is just targeted for embedded devices with more constrained hardware.

> I believe eChronos is just targeted for embedded devices with more constrained hardware. I guess it all depends on which meaning of IoT and embedded you are using.

No MMU is usually the differentiating constraint when there's two RTOS's. I dont use IoT because it's a BS buzzword.

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

#98

Post by felixk42 »

jkot wrote: post #14
TheMagicHorsey wrote: post #10

If the goal is to provide a verifiably correct kernel, why not build that kernel in something like OCAML so you can leverage a better type system and use the existing verification infrastructure in that language?

I think you would also have to verify resulting binary, compiler, libraries... It seems more manageable to verify a few KB of assembly or C

Exactly, and then one has to deal with the runtime and GC.

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

#99

Post by ori_b »

wolfgke wrote: post #90
pjmlp wrote: post #85

Earlier quoted context omitted.

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

Exactly this -- So, someone must have grabbed a copy of the source at that time, and I'd love to have a read through it one day.
Post reply on HN