Sadly, there is no reliable or usable freedom operating system based on a microkernel design (yet). What we have are only monolithic ones, based on the Linux kernel.
Linux, by design, does not offer the same level of security as a microkernel. It is considered obsolete; nobody would want to build an operating system from scratch based on a monolithic design in nowadays.
Proprietary competitors are on the rise. HarmonyOS, for example, is arguably the most mature general-purpose microkernel-based OS developed in China. Google’s Fuchsia is another example. If we don’t stay ahead of these developments, control over security will slip from our hands, placing it instead in the hands of large corporations or state-backed entities.
Rustify the kernel
Its preferable to re-write the kernel into more modern and secure language like rust (the entire kernel is just 10k lines in case of seL4 which considered very minimal compared to linux)
Could you elaborate on how this is particularly more secure than Qubes OS? I don’t think seL4 will be very suitable for this because of its likely very lacking hardware support (unless there’s an army of developers making networking and graphics drivers for seL4 that I don’t know about). Xen + a Linux dom0 seems like it probably gives similar levels of security to this.
Genode looks really cool, I didn’t know about it before. (Edit: Heh, looks like they’re using separate Linux VMs as both hardware and an application compatibility layers. Clever.)
Qubes is the closest design but it has its own drawbacks:
Qubes is not App-per-VM design, rather OS-per-VM
Qubes doesnt give the latest packages, Qubes relies on other OSs doing that, wether debian or fedora or…etc. So it doesnt solve the issue of anything related to packages issues (old, vulnerable…etc).
Qubes doesnt solve packages compromising user level inside OS-per-VM, so if you have a malware in your VM or got infected package, your entire OS in the appVM will be infected (and if its from the repository, so as your templateVM).
Qubes relies on merging two components which are not produced from the same developers, xen and linux, this can produce version conflicts or unwanted bugs, compared to seL4 or even qubes+kvm (even though kvm is worse than xen).
Qubes is not immutable distro.
Qubes doesnt support bootstrappable builds.
Qubes has hands to modify the distros that they have from the main distro producer/owners. So debian package case for example will be X (package developer) -> Y (debian package maintainer/s) -> Q (qubes-debian maintainer/s) -> User.
Qubes doesnt harden the connection or remove old stuff in the kernel or even harden the kernel itself.
Qubes based itself on even deprecated versions of fedora, not even stable packages. Yes they upgrade xen,kernel and some other packages to mitigate some security issues or hardware compatibilities, but the concept itself is flawed.
Qubes based on linux kernel, linux kernel is a mess and doesnt focus on security, and its insecure by design.
… etc. But what i give credit for qubes is that it contained the distros within VMs and made their packages/apps of these OSs to play with more easy with layer of security. Separation of hardware and user daily software with an offline layer. Yet there are many areas for improvements or maybe never going to be improved.
Yeah this is hard problem, thats why i said if someone made it then this is like OS dropped from heaven.
To not increase the subject into lengthy repetitive explanations, your questions are answered and can be found with search engine or AI or more reading.