Comment by darksaints
2 days ago
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.
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.
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.
The SeL4 microkernel specification assumes the use of a memory management unit, and is required by default.
https://docs.sel4.systems/projects/sel4/frequently-asked-que...
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).
2 replies →
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.
1 reply →
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.