4 Jan
2016
4 Jan
'16
2:32 p.m.
On Sun, Jan 3, 2016 at 5:43 PM, Raymond Jennings <shentino(a)gmail.com> wrote:
At least the boot process gets all the information it
needs (including the
physical addresses associated with untyped memory frames) and also gets the
master I/O capability.
On Sun, Jan 3, 2016 at 3:49 PM, Gerwin Klein <Gerwin.Klein(a)nicta.com.au>
wrote:
ATA
The important part is that the only code that can manage and alter the IOMMU
is trusted code.
https://en.wikipedia.org/wiki/Input%E2%80%93output_memory_management_unit
To say "you could put an arbitrary address" demands a clear understanding
of who "you" is. User space device drivers are only possible if the user
is trustworthy and only one instance of that user is allowed to touch the
hardware
registers or control block. IOMMU drivers are most common in video device
drivers.
IOMMU registers are limited in many ways. PAT is a cleaner model for many
things.
Mixing PAT and IOMMU management is complex.
It is hard to imagine a modern device and system without DMA today. The
most
interesting impact is processor IO is often limited to slow PIO
transactions where
DMA is an order of magnitude quicker or better on many systems. It is the
rare
IO card with enough memory to do interesting work without DMA.
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:
> 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 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
_______________________________________________
Devel mailing list
Devel(a)sel4.systems
https://sel4.systems/lists/listinfo/devel
--
T o m M i t c h e l l
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.
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.