Hello, I'm new to seL4 and I'm trying to get seL4 running on an Cortex-A7 with VE extensions (NXP IMX6UL). One of the experiments I wish to do is measure how fast I can get from POR to seL4 doing something meningful. To achive optimal boot speed I have a custom bootloader that does the bare minimum. The boot flow looks like this; 1. POR 2. Init HW 3. Load & verify blobs for trust zone and seL4 4. Jump to TEE init (OP-TEE) 5. Tee init code returns to bootloader with the CPU in HYP mode At this point we're back in the bootloader, there is no MMU, D cache or I cache active 6. Configure MMU 7. Jump to seL4 kernel entry I'm currently struggling with getting the MMU properly setup and I was hoping that someone here might shed some light on what I would need to do. I've looked at the elf-loader and from what I can understand it will setup a basic memory-mapping for the kernel only. Some of the questions that stand out in my head are : 1) How should the hand over work between the BL and seL4 with respect to setting up more mappings, for example IO memory. Should the PGD & PMD tables created by the bootloader be shared with the kernel? 2) What needs to be configured before calling the seL4 entry? Thanks, Jonas