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 <[email protected]> wrote: > > > On 26 Dec 2015, at 21:24, Corey Richardson <[email protected]> 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. > > 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. >
_______________________________________________ Devel mailing list [email protected] https://sel4.systems/lists/listinfo/devel
