You aren't able to do this in a "stock" seL4 ever. It may be possible toOn 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.
modify the kernel to allow unsafe DMA, though I don't know precisely what this
DMA in and of itself will not void any assurance if you already include the
device and driver in the TCB.