Re: [seL4] dma and sel4

DMA as such works even on the ARM platforms, it just invalidates the proof assumptions, which means you need additional trust for drivers of DMA-enabled devices. VT-d and VT-x are supported for x86 in the experimental branch of the kernel and in theory require no trust in the drivers. Note that the x86 version of the kernel is not verified, though. Probably not all motherboards with VT-d support will work, we have tested the following chipsets so far: - Intel Q35 Express - Intel 5500 We are also working on a verified ARM A15 port with virtualisation extension support, which will support DMA for devices under the SystemMMU without the need to trust their drivers, but that's still some way off. Cheers, Gerwin On 05.08.2014, at 4:21 pm, Alexander Kjeldaas wrote:

The documentation states that VT-d is supported. Is DMA supported on the Intel motherboards where VT-d is supported?

Alexander

On Tue, Aug 5, 2014 at 7:23 AM, Gerwin Klein wrote: Yes. For the verification to hold, DMA needs to be off, or the driver (and hardware) for the DMA device needs to be trusted/verified.

We're working on eliminating that for A15 with SystemMMUs, but that will be a while.

Cheers, Gerwin

On 05.08.2014, at 3:09 pm, Tim Newsham wrote:

...

Does the use of DMA invalidate security guarantees in the ARM ports (and KZM in particular) currently?

-- Tim Newsham | www.thenewsh.com/~newsham | @newshtwit | thenewsh.blogspot.com

_______________________________________________ Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel

_______________________________________________ Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel

________________________________ 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.