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/
signature.asc
Description: PGP signature
_______________________________________________ Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel
