seL4 Micro-Kernel Working Towards A General-Purpose, Multi-Server OS

[brouhaha]

all you have to do to get rid of this "misconception" is to provide microkernel, abi-compatible with linux, running just as fast. what was stopping you all those years?

If a microkernel is ABI-compatible with the Linux kernel, then by definition it isn't actually a microkernel.

[brouhaha]

will it save you from browser vulnerability? will you formally verify your browser?

Will using synthetic oil in your car engine prevent your muffler from rusting out?

Obviously having fewer kernel bugs doesn't solve all problems in other system components, but that doesn't mean that it's not worthwhile to use a kernel with fewer bugs.

[zxy_thf]

I might be crashing the party ,but how about Minix 3 as an alternative?!

I don't think Minix has any chance.
L4 family is already the Top 3, if not Top 1, widely deployed operating system, used by base stations, all iOS devices, etc.

[V1tol]

seL4 is a really nice project, i don't understand why google is redeveloping a microkernel with Fuchsia, when such a well tested microkernel is readily available.

NIH syndrome. Actually Linux suffers from it too (except for kernel)

[wkleunen]

seL4 is a really nice project, i don't understand why google is redeveloping a microkernel with Fuchsia, when such a well tested microkernel is readily available.

[pal666]

The big problem is that the community ( especially the opensource one ) sees microkernels as slow. It is a big misconception

all you have to do to get rid of this "misconception" is to provide microkernel, abi-compatible with linux, running just as fast. what was stopping you all those years?

[pal666]

The advantage of seL4 over other microkernels is that seL4 is formally verified

will it save you from browser vulnerability? will you formally verify your browser?

[pal666]

This multi-server OS would be secure, support a range of use-cases and security policies, and perform comparable to monolithic systems

in a dream

[brouhaha]

I might be crashing the party ,but how about Minix 3 as an alternative?!

The advantage of seL4 over other microkernels is that seL4 is formally verified. It has been mathematically proven to meet its specification, including enforcement of security properties. The proof is done both at the C code level and at the object code (compiler output) level. There is no other real-world kernel which has been formally verified.

[pabloski]

I might be crashing the party ,but how about Minix 3 as an alternative?!

Minix has been used as a desktop OS by hobbyists. It is used in the Intel ME. It has some nice features ( like dead servers restart ). Imho Minix is better positioned to go forward. The big problem is that the community ( especially the opensource one ) sees microkernels as slow. It is a big misconception, but very hard to die.