4 Jan
2016
4 Jan
'16
10:49 a.m.
On 26 Dec 2015, at 21:24, Corey Richardson
<corey(a)octayn.net> wrote:
On Fri, Dec 25, 2015 at 11:19:55PM -0800, Raymond Jennings wrote:
seL4 does not enforce absence of DMA. In general it’s not possible to do that, that’s why
it’s an assumption to the proof that you need to validate for your system.
Without an IOMMU, you will need to trust the drivers and the hardware of DMA-capable
devices to either not use DMA or to use it safely only.
You can lock down systems to not provide any access at all to DMA-devices, which sometimes
is enough for simple separation-style systems. There are more trade-off points in the
design space, but the trust story does become massively simpler and better when you have
IOMMU support.
With an IOMMU, seL4 is in control and you’re fine.
Cheers,
Gerwin
________________________________
The information in this e-mail may be confidential and subject to legal professional
privilege and/or copyright. National ICT Australia Limited accepts no liability for any
damage caused by this email or its attachments.
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.