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

71–80 of 99 posts

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

#71

Post by nanolith »

tptacek wrote: post #35
nanolith wrote: post #24

Earlier quoted context omitted.

If done well, formal verification of kernel level services and how these use runtime protection built in hardware can absolutely reduce the attack surface of application level code. The key is to move critical services that attackers would wish to exploit into a formally verified sandbox. That is the real power of systems like seL4, even though seL4 isn't itself really geared toward the sort of chipsets commonly used…

Can you describe this with an example of a realistic use of L4-enabled sandboxing for a single-function IoT device? (I've done some L4 work so you don't need to spend a lot of time explaining.) General purpose OSs like iOS? No question: L4 is a major win. But that's not what the discussion here is really about.

Case in point: cryptography, authentication, and authorization are each very sensitive operations which are prone to both gadget attacks and sidechannel attacks. Sandboxing these operations by creating well-defined boundaries between application code and these algorithms and protocols can ensure that application level bugs cannot creep into these critical services.

Consider, for instance, that it is possible to separate TCP/IP or wireless protocol stacks from authentication code so that, for instance, a packet fragmentation bug can't be exploited to influence authentication level decisions. This is classical defense in depth strategy, but enforced through both runtime and formal methods.

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

#72

Post by simscitizen »

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.

That is completely untrue. While the BSD syscalls are supported, Mach syscalls and Mach IPC are also heavily used, especially internally at Apple.

Just one simple example: run "sample " (where is any Cocoa application) on OS X. Pretty much every thread will have an event loop powered by CFRunLoop, and they'll all be stuck in mach_msg_trap waiting for an event to occur.

Also, pretty much any sort of semi-complicated IPC on OS X is done over Mach IPC (e.g. passing a large bitmap copy-on-write from one process to another). Take a look at the ipc directory in the Chromium source, for example.

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

#73

Post by indolering »

tptacek wrote: post #35
nanolith wrote: post #24

Earlier quoted context omitted.

If done well, formal verification of kernel level services and how these use runtime protection built in hardware can absolutely reduce the attack surface of application level code. The key is to move critical services that attackers would wish to exploit into a formally verified sandbox. That is the real power of systems like seL4, even though seL4 isn't itself really geared toward the sort of chipsets commonly used…

Can you describe this with an example of a realistic use of L4-enabled sandboxing for a single-function IoT device? (I've done some L4 work so you don't need to spend a lot of time explaining.) General purpose OSs like iOS? No question: L4 is a major win. But that's not what the discussion here is really about.

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/

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

#74

Post by hinkley »

pslam wrote: post #62
tptacek wrote: post #15

Earlier quoted context omitted.

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

I wonder if anyone will manage to create a tool for Rust that can map out code partitions, or near partitions, based on access patterns of object ownership. At some tipping point a little bit of data sharing could be refactored into message passing and finish the job right.

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

#75

Post by rayiner »

simscitizen wrote: post #72
rayiner wrote: post #66

Earlier quoted context omitted.

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.

That is completely untrue. While the BSD syscalls are supported, Mach syscalls and Mach IPC are also heavily used, especially internally at Apple. Just one simple example: run "sample " (where is any Cocoa application) on OS X. Pretty much every thread will have an event loop powered by CFRunLoop, and they'll all be stuck in mach_msg_trap waiting for an event to occur. Also, pretty much any sort of semi-complicated I…

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

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

#76

Post by Jweb_Guru »

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.

For me, SeL4's verification is important because it can actually provide formal real-time guarantees. Before SeL4, if you wanted to write a hard real-time system, you pretty much had to either forego an OS, or forego formal verification (or, usually, both). Having the option to write a RTOS without also writing a bunch of boilerplate (and probably incorrect) scheduler / resource allocation code, or dedicating a core to a task because you couldn't reason about resource consumption otherwise, is pretty exciting! Sure, it may not help much with securing normal userland applications, but in many embedded systems meeting deadlines is more important than any security functionality could be; the confinement properties are in some sense just consequences of having to reliably hit deadlines and isolate resources.

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

#77

Post by _cbsz »

rayiner wrote: post #75
simscitizen wrote: post #72

Earlier quoted context omitted.

That is completely untrue. While the BSD syscalls are supported, Mach syscalls and Mach IPC are also heavily used, especially internally at Apple. Just one simple example: run "sample " (where is any Cocoa application) on OS X. Pretty much every thread will have an event loop powered by CFRunLoop, and they'll all be stuck in mach_msg_trap waiting for an event to occur. Also, pretty much any sort of semi-complicated I…

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

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

#78

Post by nickpsecurity »

indolering wrote: post #73
tptacek wrote: post #35

Earlier quoted context omitted.

Can you describe this with an example of a realistic use of L4-enabled sandboxing for a single-function IoT device? (I've done some L4 work so you don't need to spend a lot of time explaining.) General purpose OSs like iOS? No question: L4 is a major win. But that's not what the discussion here is really about.

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.

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

#79

Post by angry_octet »

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…

If you read about the OPM hack you get an idea of the absolute ineptness and decision paralysis at work in these large organisations, and you begin to understand why you can connect to the drone with telnet and why the command centre relies on 13 year old Share Point and Active X.

OPM https://news.ycombinator.com/item?id=12457786

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

#80

Post by ori_b »

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

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?
Post reply on HN