diff --git a/include/arch/x86/arch/kernel/boot.h b/include/arch/x86/arch/kernel/boot.h
index f5b9706b3..a4f7fa057 100644
--- a/include/arch/x86/arch/kernel/boot.h
+++ b/include/arch/x86/arch/kernel/boot.h
@@ -31,7 +31,6 @@ bool_t init_sys_state(
     cpu_id_t      cpu_id,
     mem_p_regs_t  *mem_p_regs,
     ui_info_t     ui_info,
-    p_region_t    boot_mem_reuse_p_reg,
     /* parameters below not modeled in abstract specification */
     uint32_t      num_drhu,
     paddr_t      *drhu_list,
diff --git a/include/hardware.h b/include/hardware.h
index 4474ff363..6cfa8953e 100644
--- a/include/hardware.h
+++ b/include/hardware.h
@@ -49,11 +49,6 @@
 extern char ki_end[1];
 #define KERNEL_ELF_TOP ((paddr_t)ki_end)
 
-/* This symbol is generated by the linker and marks the end of boot
- * code/data in kernel image */
-extern char ki_boot_end[1];
-
-
 #endif /* __ASSEMBLER__ */
 
 #include <mode/hardware.h>
diff --git a/include/kernel/boot.h b/include/kernel/boot.h
index 25f2c3fbd..46f999e51 100644
--- a/include/kernel/boot.h
+++ b/include/kernel/boot.h
@@ -39,6 +39,8 @@ static inline bool_t is_reg_empty(region_t reg)
     return reg.start == reg.end;
 }
 
+p_region_t get_p_reg_kernel_img_boot(void);
+p_region_t get_p_reg_kernel_img(void);
 bool_t init_freemem(word_t n_available, const p_region_t *available,
                     word_t n_reserved, const region_t *reserved,
                     v_region_t it_v_reg, word_t extra_bi_size_bits);
@@ -49,7 +51,7 @@ bool_t provide_cap(cap_t root_cnode_cap, cap_t cap);
 cap_t create_it_asid_pool(cap_t root_cnode_cap);
 void write_it_pd_pts(cap_t root_cnode_cap, cap_t it_pd_cap);
 void create_idle_thread(void);
-bool_t create_untypeds(cap_t root_cnode_cap, region_t boot_mem_reuse_reg);
+bool_t create_untypeds(cap_t root_cnode_cap);
 void bi_finalise(void);
 void create_domain_cap(cap_t root_cnode_cap);
 
diff --git a/src/arch/arm/kernel/boot.c b/src/arch/arm/kernel/boot.c
index 53fe21030..233b1450f 100644
--- a/src/arch/arm/kernel/boot.c
+++ b/src/arch/arm/kernel/boot.c
@@ -42,8 +42,7 @@ BOOT_CODE static bool_t arch_init_freemem(p_region_t ui_p_reg,
                                           word_t extra_bi_size_bits)
 {
     /* reserve the kernel image region */
-    reserved[0].start = KERNEL_ELF_BASE;
-    reserved[0].end = (pptr_t)ki_end;
+    reserved[0] = paddr_to_pptr_reg(get_p_reg_kernel_img());
 
     int index = 1;
 
@@ -571,12 +570,7 @@ static BOOT_CODE bool_t try_init_kernel(
     init_core_state(initial);
 
     /* create all of the untypeds. Both devices and kernel window memory */
-    if (!create_untypeds(
-            root_cnode_cap,
-    (region_t) {
-    KERNEL_ELF_BASE, (pptr_t)ki_boot_end
-    } /* reusable boot code/data */
-        )) {
+    if (!create_untypeds(root_cnode_cap)) {
         printf("ERROR: could not create untypteds for kernel image boot memory\n");
         return false;
     }
diff --git a/src/arch/riscv/kernel/boot.c b/src/arch/riscv/kernel/boot.c
index c861a10ff..a38ac92eb 100644
--- a/src/arch/riscv/kernel/boot.c
+++ b/src/arch/riscv/kernel/boot.c
@@ -60,9 +60,7 @@ BOOT_CODE static bool_t arch_init_freemem(region_t ui_reg,
      * symbols are a reference in the kernel image window, but all allocations
      * are done in terms of the main kernel window, so we do some translation.
      */
-    res_reg[0].start = (pptr_t)paddr_to_pptr(kpptr_to_paddr((void *)KERNEL_ELF_BASE));
-    res_reg[0].end = (pptr_t)paddr_to_pptr(kpptr_to_paddr((void *)ki_end));
-
+    res_reg[0] = paddr_to_pptr_reg(get_p_reg_kernel_img());
     int index = 1;
 
     /* add the dtb region, if it is not empty */
@@ -201,10 +199,6 @@ static BOOT_CODE bool_t try_init_kernel(
     cap_t it_pd_cap;
     cap_t it_ap_cap;
     cap_t ipcbuf_cap;
-    p_region_t boot_mem_reuse_p_reg = ((p_region_t) {
-        kpptr_to_paddr((void *)KERNEL_ELF_BASE), kpptr_to_paddr(ki_boot_end)
-    });
-    region_t boot_mem_reuse_reg = paddr_to_pptr_reg(boot_mem_reuse_p_reg);
     region_t ui_reg = paddr_to_pptr_reg((p_region_t) {
         ui_p_reg_start, ui_p_reg_end
     });
@@ -428,9 +422,7 @@ static BOOT_CODE bool_t try_init_kernel(
     init_core_state(initial);
 
     /* convert the remaining free memory into UT objects and provide the caps */
-    if (!create_untypeds(
-            root_cnode_cap,
-            boot_mem_reuse_reg)) {
+    if (!create_untypeds(root_cnode_cap)) {
         printf("ERROR: could not create untypteds for kernel image boot memory\n");
         return false;
     }
diff --git a/src/arch/x86/kernel/boot.c b/src/arch/x86/kernel/boot.c
index 809a2ca20..84724098a 100644
--- a/src/arch/x86/kernel/boot.c
+++ b/src/arch/x86/kernel/boot.c
@@ -87,7 +87,6 @@ BOOT_CODE bool_t init_sys_state(
     cpu_id_t      cpu_id,
     mem_p_regs_t  *mem_p_regs,
     ui_info_t     ui_info,
-    p_region_t    boot_mem_reuse_p_reg,
     /* parameters below not modeled in abstract specification */
     uint32_t      num_drhu,
     paddr_t      *drhu_list,
@@ -113,7 +112,6 @@ BOOT_CODE bool_t init_sys_state(
 
     /* convert from physical addresses to kernel pptrs */
     region_t ui_reg             = paddr_to_pptr_reg(ui_info.p_reg);
-    region_t boot_mem_reuse_reg = paddr_to_pptr_reg(boot_mem_reuse_p_reg);
 
     /* convert from physical addresses to userland vptrs */
     v_region_t ui_v_reg;
@@ -329,7 +327,7 @@ BOOT_CODE bool_t init_sys_state(
 #endif
 
     /* create all of the untypeds. Both devices and kernel window memory */
-    if (!create_untypeds(root_cnode_cap, boot_mem_reuse_reg)) {
+    if (!create_untypeds(root_cnode_cap)) {
         return false;
     }
 
diff --git a/src/arch/x86/kernel/boot_sys.c b/src/arch/x86/kernel/boot_sys.c
index e6679c952..7f1a4db1f 100644
--- a/src/arch/x86/kernel/boot_sys.c
+++ b/src/arch/x86/kernel/boot_sys.c
@@ -143,8 +143,6 @@ BOOT_CODE static paddr_t load_boot_module(word_t boot_module_start, paddr_t load
 
 static BOOT_CODE bool_t try_boot_sys_node(cpu_id_t cpu_id)
 {
-    p_region_t boot_mem_reuse_p_reg;
-
     if (!map_kernel_window(
             boot_state.num_ioapic,
             boot_state.ioapic_paddr,
@@ -164,10 +162,6 @@ static BOOT_CODE bool_t try_boot_sys_node(cpu_id_t cpu_id)
     }
 #endif
 
-    /* reuse boot code/data memory */
-    boot_mem_reuse_p_reg.start = KERNEL_ELF_PADDR_BASE;
-    boot_mem_reuse_p_reg.end = kpptr_to_paddr(ki_boot_end);
-
     /* initialise the CPU */
     if (!init_cpu(config_set(CONFIG_IRQ_IOAPIC) ? 1 : 0)) {
         return false;
@@ -178,7 +172,6 @@ static BOOT_CODE bool_t try_boot_sys_node(cpu_id_t cpu_id)
             cpu_id,
             &boot_state.mem_p_regs,
             boot_state.ui_info,
-            boot_mem_reuse_p_reg,
             /* parameters below not modelled in abstract specification */
             boot_state.num_drhu,
             boot_state.drhu_list,
@@ -347,8 +340,7 @@ static BOOT_CODE bool_t try_boot_sys(void)
     p_region_t ui_p_regs;
     paddr_t load_paddr;
 
-    boot_state.ki_p_reg.start = KERNEL_ELF_PADDR_BASE;
-    boot_state.ki_p_reg.end = kpptr_to_paddr(ki_end);
+    boot_state.ki_p_reg = get_p_reg_kernel_img();
 
     if (!x86_cpuid_initialize()) {
         printf("Warning: Your x86 CPU has an unsupported vendor, '%s'.\n"
diff --git a/src/kernel/boot.c b/src/kernel/boot.c
index 3f87297fb..4715f6d24 100644
--- a/src/kernel/boot.c
+++ b/src/kernel/boot.c
@@ -23,6 +23,26 @@ BOOT_BSS ndks_boot_t ndks_boot;
 BOOT_BSS rootserver_mem_t rootserver;
 BOOT_BSS static region_t rootserver_mem;
 
+/* Returns the physical region of the kernel image boot part, which is the part
+ * that is no longer needed once booting is finished. */
+extern char ki_boot_end[1];
+BOOT_CODE p_region_t get_p_reg_kernel_img_boot(void)
+{
+    return (p_region_t) {
+        .start = kpptr_to_paddr((const void *)KERNEL_ELF_BASE),
+        .end   = kpptr_to_paddr(ki_boot_end)
+    };
+}
+
+/* Returns the physical region of the kernel image. */
+BOOT_CODE p_region_t get_p_reg_kernel_img(void)
+{
+    return (p_region_t) {
+        .start = kpptr_to_paddr((const void *)KERNEL_ELF_BASE),
+        .end   = kpptr_to_paddr(ki_end)
+    };
+}
+
 BOOT_CODE static void merge_regions(void)
 {
     /* Walk through reserved regions and see if any can be merged */
@@ -739,8 +759,7 @@ BOOT_CODE static bool_t create_untypeds_for_region(
     return true;
 }
 
-BOOT_CODE bool_t create_untypeds(cap_t root_cnode_cap,
-                                 region_t boot_mem_reuse_reg)
+BOOT_CODE bool_t create_untypeds(cap_t root_cnode_cap)
 {
     seL4_SlotPos first_untyped_slot = ndks_boot.slot_pos_cur;
 
@@ -774,7 +793,11 @@ BOOT_CODE bool_t create_untypeds(cap_t root_cnode_cap,
         }
     }
 
-    /* if boot_mem_reuse_reg is not empty, we can create UT objs from boot code/data frames */
+    /* There is a part of the kernel (code/data) that is only needed for the
+     * boot process. We can create UT objects for these frames, so the memory
+     * can be reused.
+     */
+    region_t boot_mem_reuse_reg = paddr_to_pptr_reg(get_p_reg_kernel_img_boot());
     if (!create_untypeds_for_region(root_cnode_cap, false, boot_mem_reuse_reg, first_untyped_slot)) {
         printf("ERROR: creation of untypeds for recycled boot memory"
                " [%"SEL4_PRIx_word"..%"SEL4_PRIx_word"] failed\n",