Does the use of DMA invalidate security guarantees in the ARM ports (and KZM in particular) currently?
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 tim.newsham@gmail.com 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
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 gerwin.klein@nicta.com.au 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 tim.newsham@gmail.com 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
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 ak@formalprivacy.com 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 gerwin.klein@nicta.com.au 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 tim.newsham@gmail.com 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.
-
Alexander Kjeldaas -
Gerwin Klein -
Gerwin Klein
-
Tim Newsham