I have questions about the device drivers in the virtual machine on ARM seL4. The virtual machine on TK1 board is located on the physical memory starting at 0xb0000000. However, the MMIOs used by the device drivers in the VM are below 0xb0000000. 

1.If my understanding is correct, does that mean that a device driver in the VM can actually access a memory block outside of the VM's boundary even though it is mmio.

2. If the device driver actually uses the mmio outside of the VM's memory boundary, do the page tables (including EPT) need to map to this mmio? However, I can not find any code doing the mapping. 

Do I miss something?

Thanks

Peng