"The World's Most Highly-Assured OS" Kernel Open-Sourced

[liam]

It's that "theory vs practice" thing again. A proper micro-kernel is a thing of beauty from an architecture perspective - but keeping that purity of architecture means you can't make the compromises and shortcuts that are needed to achieve adequate performance. Monoliths have their own problems, of course, but by not enforcing strict interfaces between modules, they can avoid an awful lot of overhead...

Read up on l4 based kernels. They are completely practical. That might very well be the most used kernel arch in the world (a 2012 gd blog put the official deployment numbers at 1.5 billion).
The IPC latency for l4 kernels can be FAST.

[silix]

It's that "theory vs practice" thing again.

not really - or better, the kernel world is not that "black or white" anymore
plus, the OP referred to HURD as a general proof of failure for microkernels in general - but if anything, HURD only proved that stallman and his minions arent able to successfully develop a microkernel based OS and make it mainstream (with the model they're still adhering to, being tied to early 90's microkernel technology because of them not knowing any better)
but other microkernels have built upon the mistakes and inefficiencies of legacy Mach, distanced themselves a lot from it and strived quite a bit, although in specific niches (rt critical systems typically run on microkernels rather than linux) wouldn exactly call it a failure though..

A proper micro-kernel is a thing of beauty from an architecture perspective -

maybe, if you just look at the kernel alone and equate beauty with minimalism.. from an engineering perspective things get quite less rosy when you consider that code that would otherwise belong to the kernel ("drivers", resource arbitration facilities and so on (*)) is still there, together with more (kernel - and user -) non trivial code needed to support the former in running in its own process, be restartable etc
so the overall view on the OS core (what needs to be present at very least to allow a process to run- which now includes much more than just the kernel) may even be less clean than before

(*) resource (cpu cycles, memory, files or storage devices, io ports) sharing and arbitration need to be done anyway - but centralising "drivers" and the rest of it in the kernel allows to implement it in an efficient way that also allows the kernel to be sufficient (load the kernel and you're ready to run non core processes - not so with microkernels)
that's why it's put it beneath the kernel to userpace barrier in a pragmatic, rather than elegant, design ..

but keeping that purity of architecture means you can't make the compromises and shortcuts that are needed to achieve adequate performance.

otoh, it's to be noted that microkernels existed that achieved better performance than certain monolithic ones.. fanboyisms apart, it's all a matter of algorithms really, and how much processing a system call takes compared to the overhead of the client server round trip overhad
consider that during time, microkernels have tacked and sometimes very cleverly solved the ipc overhead problem - something linux has yet to discover as a problem, much less solve (KDBUS still does copy across address spaces and marshaling/demarshaling whereas other systems directly share argument stacks)

Monoliths have their own problems, of course, but by not enforcing strict interfaces between modules, they can avoid an awful lot of overhead...

and otoh, dont assume that just because linux isnt, no other monolithic/hybrid kernel is or can be internally compartmentalized with well defined api's...

[Delgarde]

I don't get this obsession with micro kernels. GNU Hurd basically showed that micro kernels fail hard and they're not usable for real world.

It's that "theory vs practice" thing again. A proper micro-kernel is a thing of beauty from an architecture perspective - but keeping that purity of architecture means you can't make the compromises and shortcuts that are needed to achieve adequate performance. Monoliths have their own problems, of course, but by not enforcing strict interfaces between modules, they can avoid an awful lot of overhead...

[jayrulez]

Sorry but no. I think for IoT we need security enhanced Linux + lightweight x86 hardware. Imagine a < 1W TDP and power of fastest Celerons. Possible in few years. I don't get this obsession with micro kernels. GNU Hurd basically showed that micro kernels fail hard and they're not usable for real world. Besides, there's no driver code for these. Even BSD is better.

You don't seem to know what you are talking about.

[caligula]

Those l4 kernels are pretty impressive. These are what we need for IoT, along with rewritten userspace in "safe language" (for some value of safe). The BIG job will be rewriting drivers (at least certain drivers for devices like network adaptors (including Bluetooth)) so as to make the system as reliable as possible.
The Genode framework is almost perfect for this sort of project but its security isn't there yet.

Sorry but no. I think for IoT we need security enhanced Linux + lightweight x86 hardware. Imagine a < 1W TDP and power of fastest Celerons. Possible in few years. I don't get this obsession with micro kernels. GNU Hurd basically showed that micro kernels fail hard and they're not usable for real world. Besides, there's no driver code for these. Even BSD is better.

[liam]

Those l4 kernels are pretty impressive. These are what we need for IoT, along with rewritten userspace in "safe language" (for some value of safe). The BIG job will be rewriting drivers (at least certain drivers for devices like network adaptors (including Bluetooth)) so as to make the system as reliable as possible.
The Genode framework is almost perfect for this sort of project but its security isn't there yet.

[jayrulez]

You can always use DDEKit with linux drivers on an L4 kernel; probably not without possible bugs, but if you're doing something like that you would probably have time to check for bugs yourself.

It's not a given that DDEKit works for any L4 kernel. seL4 currently does not use/support DDEKit. DDEKit is used with older and newer versions of Fiasco, Minix, Hurd and Genode. Note that DDEKit is different for each of these OS/Kernels.

[Nobu]

You can always use DDEKit with linux drivers on an L4 kernel; probably not without possible bugs, but if you're doing something like that you would probably have time to check for bugs yourself.

[log0]

I don't think the aim the same hardware coverage. Drivers alone are a huge part of linux kernel.

Yeah, microkernels as this one will usually be running drivers in user space anyway.

[jayrulez]

Thanks, wow that's quite something. A quick google search shows the Linux kernel was over 15million lines of code in 2011. I suppose it's a lot easier to keep code secure when there's so few moving parts.

For limited use cases I'm sure this would be good to use. Though with so few lines of code I'm assuming there's no hardware drivers. Imagine getting wi-fi up-and-running using this!

There are a few drivers available for various platforms. The drivers are run in userspace so so they do not add to the complexity of the kernel. With the right layers above, it could be used for the same scenarios that Linux is used for. Of course, platform, libraries and driver support aren't even near the same level that Linux is.