Hi Wladislav, The short answer is that LPAE is not currently used or supported by seL4 and so you will not be able to describe physical memory that resides above 4gb to it. Adrian On Fri 13-Jan-2017 12:20 AM, Wladislav Wiebe wrote: Hello, I am trying to integrate TI Keystone 2 platform to seL4. What I have done so far is basically an initial port of the Kernel/libs/elfloader/Platform components and introducing a new keystone defconfig. Relevant config parts about the setup: CONFIG_ARCH_ARM_V7A=y CONFIG_ARCH_ARM=y CONFIG_ARCH_AARCH32=y CONFIG_ARM_CORTEX_A15=y CONFIG_PLAT_KEYSTONE=y At the end I am able to generate an image which looks like: $ arm-cortexa15-linux-gnueabihf-readelf -e images/sel4test-driver-image-arm-keystone ELF Header: Class: ELF32 .. Entry point address: 0xc0008000 .. (I am using the same entry point as Linux use it) So far, it stops booting in the elfloader -- output log: .. [ 29.705] ## Starting application at 0xc0008000 ... ELF-loader started on CPU: ARM Ltd. Cortex-A15 r2p4 paddr=[c0008000..c032841f] -> Stop here <- Seems it stops loading @ elf_getMemoryBounds(). I suppose it is related to fact that the physical start address starts @ 0x840000000 which is beyond 32 Bit - so, LPAE support is required. The physical RAM setup looks like: bank 0: addr: 0x840000000 size: 0x17ec5000 (382 MB) bank 1: addr: 0x880000000 size: 0x80000000 (2048 MB) Do you have an idea if this is supposed to be supported on seL4? What should be the "physBase" and the "kernelBase" for such a setup? How should the "static const p_region_t BOOT_RODATA avail_p_regs" looks like? Thanks in advance!