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

[phoronix]

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

The seL4 micro-kernel that has been in development for over a decade saw the creation of the seL4 Foundation last year to further the project's goals. In 2020 the seL4 micro-kernel also added RISC-V as one of its primary CPU architectures...

http://www.phoronix.com/scan.php?page=news_item&px=seL4-Microkernel-In-2021

[waxhead]

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

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

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

[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

[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]

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?

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

[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)

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