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

51–60 of 99 posts

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

#51

Post by hughw »

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.

Where does one go to learn these formal methods?

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

#52

Post by cmrx64 »

eternalban wrote: post #48
cmrx64 wrote: post #40

Earlier quoted context omitted.

That's not what isolation is meant here: if there is a connection between applications that allows cap transfer, they aren't isolated at the cap level. See www.nicta.com.au/pub?doc=7371 for more details, page 35 ("Authority Confinement and Integrity"). If there is any shared memory or potential for shared memory via the vspace caps, there can still be info flows (see page 38, "Confidentiality: Information-flow securi…

Thanks. Skimming that, I got that (a) PHigh -> PLow via overt channels will be degraded, and that (b) seL4 reduces the attack surface to "covert channels" only which seem to be confined to H/W "platform" concerns.

There are more papers coming out soon about eliminating covert channels at the design/kernel level!

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

#53

Post by elihu »

hughw wrote: post #51
tptacek wrote: post #3

Earlier quoted context omitted.

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.

Where does one go to learn these formal methods?

I'm not very knowledgeable in this area and haven't used these tools myself, but you could start by looking into theorem-proving tools like coq and agda.

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

#54

Post by cmrx64 »

hughw wrote: post #51
tptacek wrote: post #3

Earlier quoted context omitted.

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.

Where does one go to learn these formal methods?

Depends on what level of detail you're interested in. You could check out ADA/Spark or Dafny. Or, investigate something like Isabelle/HOL or Coq - perhaps via http://concrete-semantics.org/ or http://adam.chlipala.net/cpdt/.

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

#55

Post by cmrx64 »

wyager wrote: post #43
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?

They did. There's an Isabelle spec, a Haskell implementation, and a C implementation which I believe is mechanically generated from the Haskell implementation.

The C code is manually written.

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

#56

Post by tptacek »

cvwright wrote: post #46
shandor wrote: post #4

Earlier quoted context omitted.

Sure, it's not a panacea. But at least it gives a much better foundation than what we usually are having now.

Comments in this thread also illustrate why it's hard (and frustrating) to do constructive work in security. It's a big, complicated problem, and nobody's happy unless you solve it all at once. You could do the equivalent of solving world hunger and world peace, but unless you also give everyone in the world a free puppy, you're going to get bad reviews complaining about the lack of puppies. And there's always someon…

I hope I'm not in this instance coming across that way! I like L4!

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

#57

Post by XparXnoiAx »

nickpsecurity wrote: post #44
XparXnoiAx wrote: post #26

Earlier quoted context omitted.

At DefCon, someone did a talk investigating the wireless security of some drones. Some of them had a TELNET port open for anyone to log in. The problem here isn't a lack of formal verification, it's a lack of people caring. There is only one thing that will fix the problem, and that is when corporations get hit in the wallet for having security flaws, see for example: https://medium.com/@xParXnoiAx/irresponsible-disc…

Yeah, the feeds are sent unencrypted, command centers keep getting infected due to running Windows instead of least-privilege architecture, probably written in unsafe languages, not using parser/protocol toolkits that reduce 0-days there, and I'm sure more I'll find out soon. Yeah, the companies' financial incentive is to ignore the stuff since they'll get the contracts anyway. They're just paying for capabilities ra…

To the point that sometimes, it seems they go out of their way to make things insecure...........

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

#58

Post by Animats »

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 chain of linked buffers, one side may be able to screw up the other side. If that's how you talk to the file system, it may be possible to attack the file system process that way. This won't crash the kernel.

Because L4's API is so limited, it's used mostly as a VM, with the usual bloated Linux kernel on top. QNX has only a few more kernel features than modern L4, but it can implement the POSIX API with just support in the C library. When you call "write()" from C/C++ in QNX, the C library makes a MsgSend request which is directed to a file system service, device service, or network service. The code for this is tiny. When you call "write()" from C/C++ on L4, you're usually just making a Linux system call to an ordinary big Linux in a VM. Eventually that Linux talks to other processes which do the physical disk I/O. The problem is that the giant Linux kernel is still there, just a bit more isolated from the hardware. The total amount of code that can break has not been reduced significantly.

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

#59

Post by derefr »

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?

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

#60

Post by nickpsecurity »

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?

L4 was created partly due to how much Mach failed in performance and such. The first generation by Liedkte was something like 5 times faster in overhead than Mach solutions hosting Linux. I haven't timed the recent ones but there's numbers of Mach vs L4 in here:

http://ts.data61.csiro.au/publications/papers/Heiser_10:iids...

Post reply on HN