I agree that SeL4 won't replace Linux anytime soon, but I beg to differ on the benefits of a microkernel, formally verified or not.
Any ordinary well-designed microkernel gives you a huge benefit: process isolation of core services and drivers. That means that even in the case of an insecure and unverified driver, you still have reasonable expectations of security. There was an analysis of Linux CVE's a while back and the vast majority of critical Linux CVEs to that date would either be eliminated or mitigated below critical level just by using a basic microkernel architecture (not even a verified microkernel). Only 4% would have remained critical.
The benefit of a verified microkernel like SeL4 is merely an incremental one over a basic microkernel like L4, capable of capturing that last 4% and further mitigating others. You get more reliable guarantees regarding process isolation, but architecturally it's not much different from L4. There's a little bit of clunkiness for writing userpace drivers for SeL4 that you wouldn't have for L4. That's what the LionsOS project is aiming to fix.
Process isolation of drivers is just not very useful when the driver is interfacing with a device that has full access to system memory. Which is the case for many devices today unless you use IOMMU to prevent this.
IOMMU, not regular (CPU) MMU. The FAQ _does_ address this, but it's under "What about DMA?". In short: drivers have to be trusted for now, except that there's experimental support for x86 VT-d (which is a type of IOMMU).
I've been developing a notion that, in modern times, a microkernel is not the sole root of trust. It is just the most privileged component that glues other essential components. Without it, things fall apart, but we still need quality in the "business logic" components (everything else, from this view). So a user should deploy a trusted microkernel with trusted means of download and whatever opsec, and similarly for other crucial components like drivers.
This is all essential trust anyways. The leaps and bounds we've achieved through hardware engineering have the burden that they aren't credible for security. You can use IOMMU, but perhaps I won't. Integrated co-development of hardware and software is ideal, but generally there is an adversarial relationship, and we must reflect that in the software. Trust and security are not yes/no questions. We have to keep pushing boundaries. seL4 is a good start; let's make more from it.
Not memory management unit (MMU), but I/O memory access management unit (IOMMU). That is, can a device start a DMA transfer from/to anywhere in the physical RAM? Does this access have to pass through virtual address translation? For stuff like GPUs and even NICs the performance implications can be noticeable.
Yeah, not a big fan either. I also saw some suggestion that current implementations of IOMMUs aren't highly secure. Performance is always the big opponent to security. I wrote about my thoughts on not necessarily relying on IOMMUs adjacent to this reply: https://news.ycombinator.com/item?id=43122900.
Your view is not espoused enough. Thank you for this comment. I'm not suggesting we just go and use seL4 myself, but it's a strong foundation that shows we don't have to be so cynical about the potential of microkernels.
Any ordinary well-designed microkernel gives you a huge benefit: process isolation of core services and drivers. That means that even in the case of an insecure and unverified driver, you still have reasonable expectations of security. There was an analysis of Linux CVE's a while back and the vast majority of critical Linux CVEs to that date would either be eliminated or mitigated below critical level just by using a basic microkernel architecture (not even a verified microkernel). Only 4% would have remained critical.
https://microkerneldude.org/2018/08/23/microkernels-really-d...
The benefit of a verified microkernel like SeL4 is merely an incremental one over a basic microkernel like L4, capable of capturing that last 4% and further mitigating others. You get more reliable guarantees regarding process isolation, but architecturally it's not much different from L4. There's a little bit of clunkiness for writing userpace drivers for SeL4 that you wouldn't have for L4. That's what the LionsOS project is aiming to fix.