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.
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.
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.
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."
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:
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 <process>" (where <process> 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.
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.
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.