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 <[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. > > > 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/ >
_______________________________________________ Devel mailing list [email protected] https://sel4.systems/lists/listinfo/devel
