diff --git a/elfloader-tool/include/arch-arm/64/mode/aarch64.h b/elfloader-tool/include/arch-arm/64/mode/aarch64.h
index e46611c4..89fdcfd6 100644
--- a/elfloader-tool/include/arch-arm/64/mode/aarch64.h
+++ b/elfloader-tool/include/arch-arm/64/mode/aarch64.h
@@ -63,3 +63,5 @@
 #define MT_NORMAL         4
 #define MT_NORMAL_WT      5
 #define MAIR(_attr, _mt)  ((_attr) << ((_mt) * 8))
+
+#define IS_DEV_MEM_INDEX(_idx) ((_idx) <= MT_DEVICE_GRE)
diff --git a/elfloader-tool/include/elfloader_common.h b/elfloader-tool/include/elfloader_common.h
index 7a54c316..c80f143c 100644
--- a/elfloader-tool/include/elfloader_common.h
+++ b/elfloader-tool/include/elfloader_common.h
@@ -14,7 +14,7 @@ typedef uintptr_t vaddr_t;
 
 #define PAGE_BITS           12
 
-#define BIT(x)              (1 << (x))
+#define BIT(x)              (1ul << (x))
 #define MASK(n)             (BIT(n) - 1)
 #define MIN(a, b)           (((a) < (b)) ? (a) : (b))
 #define IS_ALIGNED(n, b)    (!((n) & MASK(b)))
diff --git a/elfloader-tool/src/arch-arm/64/mmu.c b/elfloader-tool/src/arch-arm/64/mmu.c
index d5169e61..fc9a5a39 100644
--- a/elfloader-tool/src/arch-arm/64/mmu.c
+++ b/elfloader-tool/src/arch-arm/64/mmu.c
@@ -30,7 +30,11 @@ void init_boot_vspace(struct image_info *kernel_info)
     _boot_pgd_down[0] = ((uintptr_t)_boot_pud_down) | BIT(1) | BIT(0); /* its a page table */
 
     for (i = 0; i < BIT(PUD_BITS); i++) {
+        /* For exec-never bit(s), see Table D8-46 for EL2 translation regime (TR)
+         * and Table D8-45 for all others.*/
         _boot_pud_down[i] = (i << ARM_1GB_BLOCK_BITS)
+                            | BIT(54) /* UXN */
+                            | BIT(53) /* PXN */
                             | BIT(10) /* access flag */
                             | (MT_DEVICE_nGnRnE << 2) /* strongly ordered memory */
                             | BIT(0); /* 1G block */
@@ -68,7 +72,10 @@ void init_hyp_boot_vspace(struct image_info *kernel_info)
     _boot_pgd_down[0] = ((uintptr_t)_boot_pud_down) | BIT(1) | BIT(0);
 
     for (i = 0; i < BIT(PUD_BITS); i++) {
+        /* For exec-never bit(s), see Table D8-46 for EL2 translation regime (TR)
+         * and Table D8-45 for all others. Note: for EL2 TR, PXN (bit 53) is RES0. */
         _boot_pud_down[i] = (i << ARM_1GB_BLOCK_BITS)
+                            | BIT(54) /* UXN */
                             | BIT(10) /* access flag */
                             | (MT_DEVICE_nGnRnE << 2) /* strongly ordered memory */
                             | BIT(0); /* 1G block */