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
DMA in and of itself will not void any assurance if you already include the
device and driver in the TCB.