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 <corey@octayn.net> wrote:
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/