26 Dec
2015
26 Dec
'15
6:19 p.m.
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(a)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/