Speaking of which, how exactly does seL4 enforce no dma on systems without
an IOMMU?
Also, what if the DMA controllers had its own device driver and the seL4
kernel could be instructed to do the DMA buffer management itself and
simply not allow any "userland" code to touch the DMA controller? Maybe if
you have an untyped memory cap you can pass it to the kernel and ask it to
be "mapped" to the dma controller.
On Fri, Dec 25, 2015 at 10:14 PM, Corey Richardson
On Fri, Dec 25, 2015 at 03:28:07PM -0800, Raymond Jennings wrote:
Is it ever possible for seL4 to run on a conventional machine without an IOMMU if any code that manipulates a DMA capable device is included as trusted or does DMA automatically void any assurance?
Reason for question: Running seL4 on a system without an IOMMU.
You aren't able to do this in a "stock" seL4 ever. It may be possible to modify the kernel to allow unsafe DMA, though I don't know precisely what this would entail.
DMA in and of itself will not void any assurance if you already include the device and driver in the TCB.
-- cmr +16032392210 http://octayn.net/