seL4 Microkernel Being Ported To RISC-V

[phoronix]

Phoronix: seL4 Microkernel Being Ported To RISC-V

The seL4 micro-kernel that is focused on delivering robust security and performance is being ported to the RISC-V architecture...

http://www.phoronix.com/scan.php?page=news_item&px=seL4-Coming-To-RISC-V

[Mavman]

Can someone build a decent Desktop OS on top of this kernel already?!

I mean, Linux is great and all... but this... this is whole a different story

[kylew77]

How does the security of a microkernel OS like sel4 compare to say a monolithic security focused project like OpenBSD? Is sel4 a competent desktop workstation OS? Can I run firefox on it and browse the web, does it support modern many core processors? I just don't hear much about the microkernel OSes other than in embedded systems and if sel4 is anything like GNU Hurd then hardware compatibility is sure to be lacking.

[microcode]

How does the security of a microkernel OS like sel4 compare to say a monolithic security focused project like OpenBSD? Is sel4 a competent desktop workstation OS? Can I run firefox on it and browse the web, does it support modern many core processors? I just don't hear much about the microkernel OSes other than in embedded systems and if sel4 is anything like GNU Hurd then hardware compatibility is sure to be lacking.

seL4 is mostly just the kernel, and the kernel is much much smaller. If you want a full system, you are going to need device drivers and system services like filesystems and network stacks. One project that is building much of this on top of seL4 (and other kernels) is Genode.

I think it would be interesting to see some system components up to the same standard as the kernel, but that's a really high standard.

As for comparisons to OpenBSD; well, OpenBSD is a very high-quality piece of software, but there's no comparison really in terms of quality. seL4 is tiny, and it took something like a decade to get it where it is. If hardware continues to offload complexity on software, drivers will probably always be a source of quality issues.