Actually I just read some stuff in the manual.
Section 9.2 does give the boot process information on physical addresses
corresponding to physical frames of memory.
I suppose this would do, and also seems to imply that lack of an IOMMU only
voids the assurance warranty.
On Sat, Dec 26, 2015 at 2:24 AM, Corey Richardson <corey(a)octayn.net> wrote:
On Fri, Dec 25, 2015 at 11:19:55PM -0800, Raymond
Jennings wrote:
Speaking of which, how exactly does seL4 enforce
no dma on systems
without
an IOMMU?
I've been unable to determine this myself. Consider the example of an ATA
controller: it seems you could put any arbitrary address in the PRDT and
have
it spray disk contents into physical memory. In this case, all one needs
is an
IOPort for that device's range on the IO bus and potentially for its place
in
PCI configuration space (to enable bus mastering).
The manual seems to be self-contradictory here. In the section about the
BootInfo it indicates that the physical addresses are given to initiate DMA
when no IOMMU is present, but the IOSpace section states that to use DMA an
IOMMU must be used.
I can't really find any way that this is enforced or could be enforced by
the
kernel. In userland it can be done quite easily by just not giving out
IOPorts.
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.
Most DMA these days doesn't happen through any centralized "DMA
controller",
but rather each device on the PCIe network can do DMA on its own if it is
enabled as a "bus master". This is why the IOMMU is critical - it provides
a
single mechanism to enforce memory access policy when all sorts of devices
want to access memory, possibly without any other interaction with the host
CPU.
--
cmr
+16032392210
http://octayn.net/