No idea. Keep in mind that using a micro kernel is a re-think from the ground up. So not trivial and most likely beyond the resources that Qubes has available.
I see that the Hurd project themselves now describe Hurd as a research project. Previously they were a bit more inspirational and less pragmatic.
They also state that no successful general use desktop OS has ever been developed using a micro kernel. I guess it depends on your definition of success, but the Mach kernel that Hurd uses was also the kernel that NeXTSTEP used, when Apple purchased NeXT and created MacOS/OSX based on it. Apple ended up ripping out the Mach kernel and using the FreeBSD kernel. So even a company with lots of resources felt that the easier path was to go with an off the shelf monolithic kernel instead.
Keep in mind that using a micro kernel is a re-think from the ground up.
So is this thread.
Appleās goals, actions and the results of them are quite different from those of Qubes OS. I believe it is ideas that should attract resources, not he other way around (which does not mean resources donāt matter). But maybe thatās too philosophical for this forum
Microkernels are promising. Additional keyword is ācapabilityā (as in capability-based security). Capabilities are objects/handles that, by virtue of being held, confer permissions. File descriptors in UNIX-likes are close to being full capabilities; if you have a file descriptor then you must have been validated to have a good identity! Unfortunately, UNIX-likes and notably Linux donāt take it far enough. Capsicum is an attempt to bridge the gap.
seL4 is famous as a formally verified microkernel. Unfortunately it seems like seL4-the-project isnāt suitable, but a similar microkernel is viable. Of course, that requires lots of effort and money, so yeahā¦ Honestly, Iām a bit confused as to why everyone seems to treat seL4 usage as all-or-nothing. While a port would sacrifice the formal verification, I imagine the result would still be leagues ahead of monolithic OSes and a solid microkernel contender, in terms of security. 80% of the security for 20% of the effort, or whatever. (Can I just say how much I love meming the 80/20 principle? It sounds believable even when thereās no data to back it up.)
While microkernels in general have indeed not found success in mainstream computing, they are becoming more visible (or so Iād like to think). In the big three, Windows, Mac, and Linux, userspace drivers have gotten more focus. The primary downside is, of course, performance.
Performance is generally the bane of microkernels, but a microkernel as well-engineered as seL4 has exceeded expectations immensely, I would say. There is definitely a lot of ground-up reengineering to be done, but microkernels are undoubtedly the correct direction for security, and I think they will be more and more viable as time goes on. There will be some unavoidable performance loss, but the industry as a whole needs to pivot on the performance vs. security conflict anyways.
See also (partly relevant, partly broader interest in OS innovation that may end up being relevant):
exokernels
unikernels - MirageOS (unikernels galore! DispVM improvement probably)
multikernels - Barrelfish (implications for full chip coverage, not just the CPU)
capability systems - EROS, KeyKOS, CHERI
language-safe OS (not sure of proper term) - Singularity/Midori, Theseus, Redleaf
