Speaking of which, how exactly does seL4 enforce no dma on systems without an IOMMU? 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. On Fri, Dec 25, 2015 at 10:14 PM, Corey Richardson wrote:

On Fri, Dec 25, 2015 at 03:28:07PM -0800, Raymond Jennings wrote:

...

Is it ever possible for seL4 to run on a conventional machine without an IOMMU if any code that manipulates a DMA capable device is included as trusted or does DMA automatically void any assurance?

Reason for question: Running seL4 on a system without an IOMMU.

You aren't able to do this in a "stock" seL4 ever. It may be possible to modify the kernel to allow unsafe DMA, though I don't know precisely what this would entail.

DMA in and of itself will not void any assurance if you already include the device and driver in the TCB.

-- cmr +16032392210 http://octayn.net/

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 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/

On 26 Dec 2015, at 21:24, Corey Richardson 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.

On Sun, Jan 3, 2016 at 5:43 PM, Raymond Jennings 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 wrote:

...

...

On 26 Dec 2015, at 21:24, Corey Richardson 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.

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.

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 Devel@sel4.systems https://sel4.systems/lists/listinfo/devel

-- T o m M i t c h e l l