Re: [seL4] questions about the address translation for a DMA driver in the ARM VM