3 ms·

The SeL4 microkernel specification assumes the use of a memory management unit, and is required by default. https://docs.sel4.systems/projects/sel4/frequently-

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-questions.html https://docs.sel4.systems/projects/sel4/frequently-asked-que...

comex 2y ago
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).
- vacuity 2y ago
  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.
- darksaints 2y ago
  Ah yes, thanks for the correction.
nine_k 2y ago
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.
- vacuity 2y ago
  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 https://news.ycombinator.com/item?id=43122900.

comex 2y ago

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

vacuity 2y ago
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.
darksaints 2y ago
Ah yes, thanks for the correction.

nine_k 2y ago

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.

vacuity 2y ago
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 https://news.ycombinator.com/item?id=43122900.