Hacker News Reader

Comment by darksaints | Hacker News Reader

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).

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.

Ah yes, thanks for the correction.

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.

Reply on news.ycombinator.com