diff --git a/repos/base-sel4/include/sel4/functions_aarch32.h b/repos/base-sel4/include/sel4/functions_aarch32.h
new file mode 100644
index 0000000000..3c171b8842
--- /dev/null
+++ b/repos/base-sel4/include/sel4/functions_aarch32.h
@@ -0,0 +1,24 @@
+/*
+ * \brief  Implementation for seL4_GetIPCBuffer on aarch32
+ * \author Alexander Boettcher
+ * \date   2023-05-23
+ */
+
+/*
+ * Copyright (C) 2023 Genode Labs GmbH
+ *
+ * This file is part of the Genode OS framework, which is distributed
+ * under the terms of the GNU Affero General Public License version 3.
+ */
+
+#ifndef _INCLUDE__SEL4__FUNCTIONS_AARCH32_H_
+#define _INCLUDE__SEL4__FUNCTIONS_AARCH32_H_
+
+LIBSEL4_INLINE_FUNC seL4_IPCBuffer *seL4_GetIPCBuffer(void)
+{
+	seL4_IPCBuffer ** ptr = nullptr;
+	asm volatile ("mrc p15, 0, %0, c13, c0, 2" : "=r"(ptr));
+	return *ptr;
+}
+
+#endif /* _INCLUDE__SEL4__FUNCTIONS_AARCH32_H_ */
diff --git a/repos/base-sel4/include/sel4/functions_x86_64.h b/repos/base-sel4/include/sel4/functions_x86_64.h
new file mode 100644
index 0000000000..3ef3cc29e8
--- /dev/null
+++ b/repos/base-sel4/include/sel4/functions_x86_64.h
@@ -0,0 +1,24 @@
+/*
+ * \brief  Implementation for seL4_GetIPCBuffer on x86_64
+ * \author Alexander Boettcher
+ * \date   2023-05-23
+ */
+
+/*
+ * Copyright (C) 2023 Genode Labs GmbH
+ *
+ * This file is part of the Genode OS framework, which is distributed
+ * under the terms of the GNU Affero General Public License version 3.
+ */
+
+#ifndef _INCLUDE__SEL4__FUNCTIONS_X86_64_H_
+#define _INCLUDE__SEL4__FUNCTIONS_X86_64_H_
+
+LIBSEL4_INLINE_FUNC seL4_IPCBuffer *seL4_GetIPCBuffer(void)
+{
+	seL4_IPCBuffer * ptr = nullptr;
+	asm volatile ("movq %%fs:0, %0" : "=r" (ptr) : :);
+	return ptr;
+}
+
+#endif /* _INCLUDE__SEL4__FUNCTIONS_X86_64_H_ */
diff --git a/repos/base-sel4/lib/mk/spec/arm/kernel-sel4.inc b/repos/base-sel4/lib/mk/spec/arm/kernel-sel4.inc
index dc9cfee611..954e2cac08 100644
--- a/repos/base-sel4/lib/mk/spec/arm/kernel-sel4.inc
+++ b/repos/base-sel4/lib/mk/spec/arm/kernel-sel4.inc
@@ -18,14 +18,36 @@ else
 SEL4_CCACHE=
 endif
 
-elfloader/elfloader.o:
+configured_kernel:
+	$(VERBOSE) cmake -DCROSS_COMPILER_PREFIX=$(CROSS_DEV_PREFIX) \
+	                 -DCMAKE_TOOLCHAIN_FILE=$(SEL4_DIR)/gcc.cmake \
+	                 -DKernelARMPlatform=sabre \
+	                 -G Ninja \
+	                 -C $(SEL4_DIR)/configs/ARM_verified.cmake \
+	                 $(SEL4_DIR) \
+	&& echo -e "\n#define CONFIG_PRINTING 1"                        >>gen_config/kernel/gen_config.h \
+	&& echo -e "#define CONFIG_DEBUG_BUILD 1"                        >>gen_config/kernel/gen_config.h \
+	&& echo -e "#define CONFIG_ENABLE_BENCHMARKS 1"                  >>gen_config/kernel/gen_config.h \
+	&& echo -e "#define CONFIG_BENCHMARK_TRACK_UTILISATION 1"        >>gen_config/kernel/gen_config.h \
+	&& echo -e "#define CONFIG_SET_TLS_BASE_SELF 1"                  >>gen_config/kernel/gen_config.h \
+	&& echo -e "#define CONFIG_HAVE_FPU 1"                           >>gen_config/kernel/gen_config.h \
+	&& echo -e "#define CONFIG_AARCH32_FPU_ENABLE_CONTEXT_SWITCH  1" >>gen_config/kernel/gen_config.h \
+	&& echo -e "#define CONFIG_FPU_MAX_RESTORES_SINCE_SWITCH  64"    >>gen_config/kernel/gen_config.h \
+	\
+	&& sed -e "s/CONFIG_NUM_DOMAINS 16/CONFIG_NUM_DOMAINS 1/"                    \
+	       -e "s/CONFIG_ROOT_CNODE_SIZE_BITS 12/CONFIG_ROOT_CNODE_SIZE_BITS 15/" \
+	          gen_config/kernel/gen_config.h   >gen_config/kernel/gen_config.tmp \
+	&& mv     gen_config/kernel/gen_config.tmp  gen_config/kernel/gen_config.h   \
+	&& touch configured_kernel
+
+elfloader/elfloader.o: configured_kernel
 	$(VERBOSE)cp -r $(TOOLS_DIR)/elfloader-tool $(LIB_CACHE_DIR)/$(LIB)/elfloader
 	$(VERBOSE)mkdir -p $(LIB_CACHE_DIR)/$(LIB)/elfloader/tools/kbuild
 	$(VERBOSE)mkdir -p $(LIB_CACHE_DIR)/$(LIB)/elfloader/include/generated
 	$(VERBOSE)ln -s $(TOOLS_DIR)/common-tool/common.mk $(LIB_CACHE_DIR)/$(LIB)/elfloader/
 	$(VERBOSE)ln -s $(TOOLS_DIR)/common-tool/files_to_obj.sh $(LIB_CACHE_DIR)/$(LIB)/elfloader/
 	$(VERBOSE)ln -s $(TOOLS_DIR)/kbuild-tool/Kbuild.include $(LIB_CACHE_DIR)/$(LIB)/elfloader/tools/kbuild/
-	$(VERBOSE)ln -s $(SEL4_DIR)/configs/$(PLAT)/$(BOARD)/autoconf.h $(LIB_CACHE_DIR)/$(LIB)/elfloader/include/generated/
+	$(VERBOSE)ln -s $(LIB_CACHE_DIR)/$(LIB)/gen_config/kernel/gen_config.h $(LIB_CACHE_DIR)/$(LIB)/elfloader/include/generated/autoconf.h
 	$(VERBOSE)$(MAKE) -C $(LIB_CACHE_DIR)/$(LIB)/elfloader \
 	          TOOLPREFIX=$(CROSS_DEV_PREFIX) \
 	          ARCH=arm PLAT=$(PLAT) ARMV=armv7-a __ARM_32__="y" \
@@ -35,7 +57,5 @@ elfloader/elfloader.o:
 	          srctree=.
 
 build_kernel: elfloader/elfloader.o
-	$(VERBOSE)$(MAKE) \
-	          TOOLPREFIX=$(CROSS_DEV_PREFIX) \
-	          BOARD=$(BOARD) ARCH=arm PLAT=$(PLAT) CPU=$(CPU) ARMV=armv7-a DEBUG=1 \
-	          SOURCE_ROOT=$(SEL4_DIR) -f$(SEL4_DIR)/Makefile
+	$(VERBOSE) ninja kernel.elf && \
+	$(CUSTOM_STRIP) -o kernel.elf.strip kernel.elf
diff --git a/repos/base-sel4/lib/mk/spec/arm/syscall-sel4-imx6q_sabrelite.mk b/repos/base-sel4/lib/mk/spec/arm/syscall-sel4-imx6q_sabrelite.mk
index 16d149b926..449c39b762 100644
--- a/repos/base-sel4/lib/mk/spec/arm/syscall-sel4-imx6q_sabrelite.mk
+++ b/repos/base-sel4/lib/mk/spec/arm/syscall-sel4-imx6q_sabrelite.mk
@@ -1,8 +1,10 @@
 PLAT := imx6
 ARCH := arm
+BOARD := imx6q_sabrelite
 
 SEL4_ARCH := aarch32
-PLAT_BOARD := /imx6q_sabrelite
 SEL4_WORDBITS := 32
 
+LIBS += kernel-sel4-imx6q_sabrelite
+
 include $(REP_DIR)/lib/mk/syscall-sel4.inc
diff --git a/repos/base-sel4/lib/mk/spec/x86_64/kernel-sel4-pc.mk b/repos/base-sel4/lib/mk/spec/x86_64/kernel-sel4-pc.mk
index 0ad8b149e0..ef86c55b71 100644
--- a/repos/base-sel4/lib/mk/spec/x86_64/kernel-sel4-pc.mk
+++ b/repos/base-sel4/lib/mk/spec/x86_64/kernel-sel4-pc.mk
@@ -11,9 +11,38 @@ else
 all:
 endif
 
-build_kernel:
-	$(VERBOSE)$(MAKE) \
-	          TOOLPREFIX=$(CROSS_DEV_PREFIX) \
-	          BOARD=x86_64 ARCH=x86 SEL4_ARCH=x86_64 PLAT=pc99 DEBUG=1 \
-	          SOURCE_ROOT=$(SEL4_DIR) -f$(SEL4_DIR)/Makefile
+configured_kernel:
+	$(VERBOSE) cmake -DCROSS_COMPILER_PREFIX=$(CROSS_DEV_PREFIX) \
+	                 -DCMAKE_TOOLCHAIN_FILE=$(SEL4_DIR)/gcc.cmake \
+	                 -G Ninja \
+	                 -C $(SEL4_DIR)/configs/X64_verified.cmake \
+	                 $(SEL4_DIR) \
+	\
+	&& echo -e "\n#define CONFIG_PRINTING 1"                  >>gen_config/kernel/gen_config.h \
+	&& echo -e "#define CONFIG_DEBUG_BUILD 1"                 >>gen_config/kernel/gen_config.h \
+	&& echo -e "#define CONFIG_VTX 1"                         >>gen_config/kernel/gen_config.h \
+	&& echo -e "#define CONFIG_ENABLE_BENCHMARKS 1"           >>gen_config/kernel/gen_config.h \
+	&& echo -e "#define CONFIG_BENCHMARK_TRACK_UTILISATION 1" >>gen_config/kernel/gen_config.h \
+	&& echo -e "#define CONFIG_ARCH_X86_GENERIC 1"            >>gen_config/kernel/gen_config.h \
+	&& echo -e "#define CONFIG_FXSAVE           1"            >>gen_config/kernel/gen_config.h \
+	&& echo -e "#define CONFIG_SET_TLS_BASE_SELF 1"           >>gen_config/kernel/gen_config.h \
+	\
+	&& sed -e "s/CONFIG_MAX_NUM_NODES 1/CONFIG_MAX_NUM_NODES 16/"                                   \
+	       -e "s/CONFIG_MAX_VPIDS 0/CONFIG_MAX_VPIDS 64/"                                           \
+	       -e "s/CONFIG_NUM_DOMAINS 16/CONFIG_NUM_DOMAINS 1/"                                       \
+	       -e "s/CONFIG_MAX_NUM_BOOTINFO_UNTYPED_CAPS 50/CONFIG_MAX_NUM_BOOTINFO_UNTYPED_CAPS 160/" \
+	       -e "s/CONFIG_FSGSBASE_INST 1/CONFIG_FSGSBASE_MSR 1/"                                     \
+	       -e "s/CONFIG_KERNEL_FSGS_BASE inst/CONFIG_KERNEL_FSGS_BASE msr/"                         \
+	       -e "/CONFIG_HUGE_PAGE/d"                                                                 \
+	       -e "/CONFIG_SUPPORT_PCID/d"                                                              \
+	       -e "/CONFIG_XSAVE 1/d"                                                                   \
+	       -e "/CONFIG_XSAVE_XSAVEOPT 1/d"                                                          \
+	       -e "/CONFIG_ARCH_X86_NEHALEM 1/d"                                                        \
+	       -e "/CONFIG_KERNEL_X86_MICRO_ARCH nehalem/d"                                             \
+	       gen_config/kernel/gen_config.h   >gen_config/kernel/gen_config.tmp \
+	&& mv  gen_config/kernel/gen_config.tmp  gen_config/kernel/gen_config.h \
+	&& touch configured_kernel
 
+build_kernel: configured_kernel
+	$(VERBOSE) ninja kernel.elf && \
+	$(CUSTOM_STRIP) -o kernel.elf.strip kernel.elf
diff --git a/repos/base-sel4/lib/mk/spec/x86_64/syscall-sel4-pc.mk b/repos/base-sel4/lib/mk/spec/x86_64/syscall-sel4-pc.mk
index a7fec89056..73ced6e6e1 100644
--- a/repos/base-sel4/lib/mk/spec/x86_64/syscall-sel4-pc.mk
+++ b/repos/base-sel4/lib/mk/spec/x86_64/syscall-sel4-pc.mk
@@ -1,11 +1,13 @@
 PLAT := pc99
 ARCH := x86
+BOARD := pc
 
 SEL4_ARCH := x86_64
-PLAT_BOARD := /$(SEL4_ARCH)
 SEL4_WORDBITS := 64
 
 ARCH_INCLUDES := exIPC.h vmenter.h
 SEL4_ARCH_INCLUDES := syscalls_syscall.h
 
+LIBS += kernel-sel4-pc
+
 include $(REP_DIR)/lib/mk/syscall-sel4.inc
diff --git a/repos/base-sel4/lib/mk/syscall-sel4.inc b/repos/base-sel4/lib/mk/syscall-sel4.inc
index af9b286d46..5382835188 100644
--- a/repos/base-sel4/lib/mk/syscall-sel4.inc
+++ b/repos/base-sel4/lib/mk/syscall-sel4.inc
@@ -10,7 +10,6 @@
 # port, if missing, is added to the missing-ports list of this stage.
 #
 LIBSEL4_DIR := $(call select_from_ports,sel4)/src/kernel/sel4/libsel4
-LIBSEL4_AUTO:= $(call select_from_ports,sel4)/src/kernel/sel4/configs/$(PLAT)$(PLAT_BOARD)
 
 #
 # Execute the rules in this file only at the second build stage when we know
@@ -29,14 +28,15 @@ SEL4_ARCH_INCLUDES += simple_types.h types.h constants.h objecttype.h \
                       functions.h syscalls.h invocation.h deprecated.h \
                       types_gen.h faults.h
 
-ARCH_INCLUDES += objecttype.h types.h constants.h functions.h deprecated.h \
+ARCH_INCLUDES += objecttype.h types.h constants.h deprecated.h \
                  syscalls.h invocation.h simple_types.h
 
 INCLUDES := objecttype.h types.h bootinfo.h bootinfo_types.h errors.h \
-            constants.h messages.h sel4.h macros.h simple_types.h \
+            constants.h sel4.h macros.h simple_types.h \
             syscall.h invocation.h shared_types_gen.h debug_assert.h \
-            shared_types.h sel4.h deprecated.h autoconf.h syscalls.h faults.h \
-            benchmark_utilisation_types.h
+            shared_types.h deprecated.h autoconf.h syscalls.h faults.h \
+            benchmark_utilisation_types.h \
+            syscalls_master.h virtual_client.h
 
 PLAT_API_INCLUDES := constants.h
 
@@ -49,6 +49,29 @@ INCLUDE_SYMLINKS += include/interfaces/sel4_client.h
 
 all: $(INCLUDE_SYMLINKS)
 
+#
+# IPCBuffer pointer are not set up by kernel anymore, instead user land has
+# to care about tracking the IPCBuffer, details are in the RFC
+#
+#   https://sel4.atlassian.net/browse/RFC-3
+#
+# The usage of the __thread variable in the original include/sel4/functions.h
+# would require our emutls emulation to work in core/roottask at an very
+# early stage, which we don't support currently.
+#
+# As workaround, we setup the tls pointer per architecture such, that it
+# points to the IPCBuffer pointer per thread, which is implemented in
+# repos/base-sel4/include/sel4/functions_$(SEL4_ARCH).h
+#
+include/sel4/sel4_arch/functions.h: $(LIBSEL4_DIR)/include/sel4/functions.h
+	$(VERBOSE)mkdir -p $(dir $@) && \
+	sed -e "s|extern __thread seL4_IPCBuffer|//extern __thread seL4_IPCBuffer|" \
+	    -e "s|#include <sel4/syscalls.h>|#include <sel4/syscalls.h>\n#include <sel4/functions_$(SEL4_ARCH).h>\n|" \
+	    -e "/LIBSEL4_INLINE_FUNC void seL4_SetIPCBuffer(seL4_IPCBuffer \*ipc_buffer)/,+4d" \
+	    -e "/LIBSEL4_INLINE_FUNC seL4_IPCBuffer \*seL4_GetIPCBuffer/,+3d" \
+	       $< >include/sel4/functions.h && \
+	touch $@
+
 #
 # Plain symlinks to existing headers
 #
@@ -60,9 +83,11 @@ include/sel4/arch/%.h: $(LIBSEL4_DIR)/arch_include/$(ARCH)/sel4/arch/%.h
 	$(VERBOSE)mkdir -p $(dir $@)
 	$(VERBOSE)ln -sf $< $@
 
-include/sel4/autoconf.h: $(LIBSEL4_AUTO)/autoconf.h
+include/sel4/autoconf.h: $(LIB_CACHE_DIR)/kernel-sel4-$(BOARD)/autoconf/autoconf.h
 	$(VERBOSE)mkdir -p $(dir $@)
 	$(VERBOSE)ln -sf $< $@
+	$(VERBOSE)mkdir include/sel4/kernel -p
+	$(VERBOSE)ln -sf $(LIB_CACHE_DIR)/kernel-sel4-$(BOARD)/gen_config/kernel/gen_config.h include/sel4/kernel/gen_config.h
 
 include/sel4/%.h: $(LIBSEL4_DIR)/include/sel4/%.h
 	$(VERBOSE)mkdir -p $(dir $@)
@@ -79,17 +104,17 @@ include/sel4/mode/types.h: $(LIBSEL4_DIR)/mode_include/$(SEL4_WORDBITS)/sel4/mod
 #
 # Generated headers
 #
-include/sel4/%.pbf: $(LIBSEL4_DIR)/include/sel4/%.bf include/sel4/autoconf.h
+include/sel4/mode_include/$(SEL4_WORDBITS)/sel4/shared_types.pbf: $(LIBSEL4_DIR)/mode_include/$(SEL4_WORDBITS)/sel4/shared_types.bf include/sel4/autoconf.h
 	$(MSG_CONVERT)$(notdir $@)
 	$(VERBOSE)mkdir -p $(dir $@)
-	$(VERBOSE)$(CPP) -P $< >$@
+	$(VERBOSE)$(CPP) -Iinclude/sel4 -P $< >$@
 
 include/sel4/sel4_arch/types.pbf: $(LIBSEL4_DIR)/sel4_arch_include/$(SEL4_ARCH)/sel4/sel4_arch/types.bf include/sel4/autoconf.h
 	$(MSG_CONVERT)$(notdir $@)
 	$(VERBOSE)mkdir -p $(dir $@)
 	$(VERBOSE)$(CPP) -Iinclude/sel4 -I$(LIBSEL4_DIR)/arch_include/$(ARCH) -P $< >$@
 
-include/sel4/shared_types_gen.h: include/sel4/shared_types_$(SEL4_WORDBITS).pbf
+include/sel4/shared_types_gen.h: include/sel4/mode_include/$(SEL4_WORDBITS)/sel4/shared_types.pbf
 	$(MSG_CONVERT)$(notdir $@)
 	$(VERBOSE)mkdir -p $(dir $@)
 	$(VERBOSE)python -B $(LIBSEL4_DIR)/tools/bitfield_gen.py \
diff --git a/repos/base-sel4/patches/address_of_packed_member.patch b/repos/base-sel4/patches/address_of_packed_member.patch
deleted file mode 100644
index e3113f61c2..0000000000
--- a/repos/base-sel4/patches/address_of_packed_member.patch
+++ /dev/null
@@ -1,50 +0,0 @@
-From 3e83f89990e356b02b227cd883d32ccafa283127 Mon Sep 17 00:00:00 2001
-From: Simon Shields <simon.shields@data61.csiro.au>
-Date: Tue, 17 Sep 2019 11:54:22 +1000
-Subject: [PATCH] x86: avoid -Waddress-of-packed-member
-
-It's safe to take the address of this member, since it's the
-first thing in a cacheline-aligned struct.
----
- include/arch/x86/arch/32/mode/stack.h | 7 ++++++-
- src/arch/x86/kernel/vspace.c          | 9 +++++++--
- 2 files changed, 13 insertions(+), 3 deletions(-)
-
-diff --git a/include/arch/x86/arch/32/mode/stack.h b/include/arch/x86/arch/32/mode/stack.h
-index 93304b96fa..e8e7f1c254 100644
---- src/kernel/sel4/include/arch/x86/arch/32/mode/stack.h
-+++ src/kernel/sel4/include/arch/x86/arch/32/mode/stack.h
-@@ -45,7 +45,12 @@ static inline void setKernelEntryStackPointer(tcb_t *target_thread)
-     /* The first item to be pushed onto the stack should always be SS */
-     register_context_top = (word_t)&target_thread->tcbArch.tcbContext.registers[SS + 1];
- 
--    tss_ptr_set_esp0(&x86KSGlobalState[CURRENT_CPU_INDEX()].x86KStss.tss, register_context_top);
-+    /*
-+     * Work around -Waddress-of-packed-member. TSS is the first thing
-+     * in the struct and so it's safe to take its address.
-+     */
-+    void *tss = &x86KSGlobalState[CURRENT_CPU_INDEX()].x86KStss.tss;
-+    tss_ptr_set_esp0(tss, register_context_top);
- 
-     if (config_set(CONFIG_HARDWARE_DEBUG_API)) {
-         x86_wrmsr(IA32_SYSENTER_ESP_MSR, register_context_top);
-diff --git a/src/arch/x86/kernel/vspace.c b/src/arch/x86/kernel/vspace.c
-index 0ff6d30fff..be9d5f6266 100644
---- src/kernel/sel4/src/arch/x86/kernel/vspace.c
-+++ src/kernel/sel4/src/arch/x86/kernel/vspace.c
-@@ -493,8 +493,13 @@ BOOT_CODE bool_t init_vm_state(void)
-         SMP_COND_STATEMENT(return false);
-     }
- 
--    init_tss(&x86KSGlobalState[CURRENT_CPU_INDEX()].x86KStss.tss);
--    init_gdt(x86KSGlobalState[CURRENT_CPU_INDEX()].x86KSgdt, &x86KSGlobalState[CURRENT_CPU_INDEX()].x86KStss.tss);
-+    /*
-+     * Work around -Waddress-of-packed-member. TSS is the first thing
-+     * in the struct and so it's safe to take its address.
-+     */
-+    void *tss_ptr = &x86KSGlobalState[CURRENT_CPU_INDEX()].x86KStss.tss;
-+    init_tss(tss_ptr);
-+    init_gdt(x86KSGlobalState[CURRENT_CPU_INDEX()].x86KSgdt, tss_ptr);
-     init_idt(x86KSGlobalState[CURRENT_CPU_INDEX()].x86KSidt);
-     return true;
- }
diff --git a/repos/base-sel4/patches/arm_no_dtb.patch b/repos/base-sel4/patches/arm_no_dtb.patch
new file mode 100644
index 0000000000..aad61c4cb2
--- /dev/null
+++ b/repos/base-sel4/patches/arm_no_dtb.patch
@@ -0,0 +1,15 @@
+--- src/kernel/sel4/src/arch/arm/kernel/boot.c
++++ src/kernel/sel4/src/arch/arm/kernel/boot.c
+@@ -582,6 +582,12 @@
+         dtb_end_p = dtb_addr_p + dtb_size;
+     }
+ 
++    /*
++     * no DTB support on Genode/seL4 - avoids assertion in
++     * src/kernel/boot.c: assert(r->start >= reserved[i - 1].end);
++     */
++    dtb_addr_p = dtb_end_p = 0;
++
+ #ifdef ENABLE_SMP_SUPPORT
+     /* we assume there exists a cpu with id 0 and will use it for bootstrapping */
+     if (getCurrentCPUIndex() == 0) {
diff --git a/repos/base-sel4/patches/autoconf_32.patch b/repos/base-sel4/patches/autoconf_32.patch
deleted file mode 100644
index fc7daf1cca..0000000000
--- a/repos/base-sel4/patches/autoconf_32.patch
+++ /dev/null
@@ -1,48 +0,0 @@
---- src/kernel/sel4/configs/pc99/autoconf.h
-+++ src/kernel/sel4/configs/pc99/autoconf.h
-@@ -51,13 +51,13 @@
- #define CONFIG_MAX_NUM_BOOTINFO_UNTYPED_CAPS 167
- #define CONFIG_FPU_MAX_RESTORES_SINCE_SWITCH 64
- #define CONFIG_LIB_SEL4_VKA_DEBUG_LIVE_SLOTS_SZ 0
--#define CONFIG_MAX_NUM_NODES 1
-+#define CONFIG_MAX_NUM_NODES 16
- #define CONFIG_CROSS_COMPILER_PREFIX ""
- #define CONFIG_LIB_SEL4_INLINE_INVOCATIONS 1
- #define CONFIG_LIB_SEL4_MUSLC_SYS 1
- #define CONFIG_HAVE_LIB_SEL4_TEST 1
- #define CONFIG_LIB_MUSL_C 1
--#define CONFIG_ARCH_X86_NEHALEM 1
-+#define CONFIG_ARCH_X86_GENERIC 1
- #define CONFIG_MAX_NUM_WORK_UNITS_PER_PREEMPTION 100
- #define CONFIG_USER_CFLAGS ""
- #define CONFIG_HAVE_LIB_SEL4_DEBUG 1
-@@ -75,13 +75,13 @@
- #define CONFIG_HAVE_LIB_SEL4_SIMPLE 1
- #define CONFIG_HAVE_LIB_ELF 1
- #define CONFIG_HAVE_LIB_PLATSUPPORT 1
--#define CONFIG_NUM_DOMAINS 16
-+#define CONFIG_NUM_DOMAINS 1
- #define CONFIG_ARCH_IA32 1
- #define CONFIG_HAVE_LIB_UTILS 1
- #define CONFIG_USER_OPTIMISATION_O2 1
- #define CONFIG_LIB_CPIO 1
- #define CONFIG_RETYPE_FAN_OUT_LIMIT 256
--#define CONFIG_ROOT_CNODE_SIZE_BITS 16
-+#define CONFIG_ROOT_CNODE_SIZE_BITS 18
- #define CONFIG_NUM_PRIORITIES 256
- #define CONFIG_TESTPRINTER_REGEX ".*"
- #define CONFIG_APP_SEL4TEST 1
-@@ -96,6 +96,13 @@
- #define CONFIG_CACHE_LN_SZ 64
- #define CONFIG_LIB_SEL4_MUSLC_SYS_MORECORE_BYTES 1048576
- #define CONFIG_BUILDSYS_USE_CCACHE 1
-+#define CONFIG_MULTIBOOT1_HEADER
-+#define CONFIG_MULTIBOOT2_HEADER
-+#define CONFIG_PRINTING 1
-+#define CONFIG_ENABLE_BENCHMARKS 1
-+#define CONFIG_BENCHMARK_TRACK_UTILISATION 1
-+#define CONFIG_VTX 1
-+#define CONFIG_MAX_VPIDS 64
- #else
- #define AUTOCONF_INCLUDED
- #define CONFIG_LIB_SEL4_SIMPLE 1
diff --git a/repos/base-sel4/patches/autoconf_64.patch b/repos/base-sel4/patches/autoconf_64.patch
deleted file mode 100644
index de290d4491..0000000000
--- a/repos/base-sel4/patches/autoconf_64.patch
+++ /dev/null
@@ -1,63 +0,0 @@
---- src/kernel/sel4/configs/pc99/autoconf.h
-+++ src/kernel/sel4/configs/pc99/autoconf.h
-@@ -129,7 +129,7 @@
- #define CONFIG_SEL4UTILS_STACK_SIZE 655360
- #define CONFIG_HAVE_LIB_SEL4_ALLOCMAN 1
- #define CONFIG_FASTPATH 1
--#define CONFIG_X2APIC 1
-+#define CONFIG_XAPIC 1
- #define CONFIG_LIB_SEL4_VKA_DEBUG_LIVE_OBJS_SZ 0
- #define CONFIG_HAVE_TIMER 1
- #define CONFIG_SEL4UTILS_CSPACE_SIZE_BITS 18
-@@ -147,7 +147,6 @@
- #define CONFIG_MAX_NUM_BOOTINFO_UNTYPED_CAPS 230
- #define CONFIG_LIB_SEL4_VKA_DEBUG_LIVE_SLOTS_SZ 0
- #define CONFIG_SYSCALL 1
--#define CONFIG_MAX_NUM_NODES 1
- #define CONFIG_CROSS_COMPILER_PREFIX ""
- #define CONFIG_MAX_RMRR_ENTRIES 32
- #define CONFIG_LIB_SEL4_INLINE_INVOCATIONS 1
-@@ -162,21 +161,20 @@
- #define CONFIG_OPTIMISATION_O2 1
- #define CONFIG_HAVE_LIB_CPIO 1
- #define CONFIG_HAVE_LIB_SEL4_VKA 1
--#define CONFIG_FSGSBASE_INST 1
-+#define CONFIG_FSGSBASE_MSR 1
- #define CONFIG_HAVE_LIB_SEL4_PLAT_SUPPORT 1
- #define CONFIG_USER_EXTRA_CFLAGS "-D_XOPEN_SOURCE=700"
- #define CONFIG_HAVE_FPU 1
- #define CONFIG_FPU_MAX_RESTORES_SINCE_SWITCH 64
- #define CONFIG_HAVE_LIB_SEL4_SIMPLE 1
- #define CONFIG_HAVE_LIB_ELF 1
--#define CONFIG_SUPPORT_PCID 1
- #define CONFIG_HAVE_LIB_PLATSUPPORT 1
--#define CONFIG_NUM_DOMAINS 16
-+#define CONFIG_NUM_DOMAINS 1
- #define CONFIG_HAVE_LIB_UTILS 1
- #define CONFIG_USER_OPTIMISATION_O2 1
- #define CONFIG_LIB_CPIO 1
- #define CONFIG_RETYPE_FAN_OUT_LIMIT 256
--#define CONFIG_ROOT_CNODE_SIZE_BITS 16
-+#define CONFIG_ROOT_CNODE_SIZE_BITS 18
- #define CONFIG_NUM_PRIORITIES 256
- #define CONFIG_TESTPRINTER_REGEX ".*"
- #define CONFIG_APP_SEL4TEST 1
-@@ -189,9 +187,16 @@
- #define CONFIG_LIBSEL4DEBUG_ALLOC_BUFFER_ENTRIES 128
- #define CONFIG_CACHE_LN_SZ 64
- #define CONFIG_ARCH_X86_64 1
--#define CONFIG_HUGE_PAGE 1
- #define CONFIG_LIB_SEL4_MUSLC_SYS_MORECORE_BYTES 1048576
- #define CONFIG_BUILDSYS_USE_CCACHE 1
--#define CONFIG_MAX_NUM_NODES 1
-+#define CONFIG_MAX_NUM_NODES 16
- #define CONFIG_KERNEL_STACK_BITS 12
-+#define CONFIG_ARCH_X86_GENERIC 1
-+#define CONFIG_MULTIBOOT1_HEADER
-+#define CONFIG_MULTIBOOT2_HEADER
-+#define CONFIG_PRINTING 1
-+#define CONFIG_ENABLE_BENCHMARKS 1
-+#define CONFIG_BENCHMARK_TRACK_UTILISATION 1
-+#define CONFIG_VTX 1
-+#define CONFIG_MAX_VPIDS 64
- #endif /* ARCH_IA32 */
diff --git a/repos/base-sel4/patches/config.patch b/repos/base-sel4/patches/config.patch
index a0dde99cba..5fd7dc7986 100644
--- a/repos/base-sel4/patches/config.patch
+++ b/repos/base-sel4/patches/config.patch
@@ -1,53 +1,22 @@
---- src/kernel/sel4/Makefile
-+++ src/kernel/sel4/Makefile
-@@ -287,8 +287,8 @@
- # Only set CFLAGS if we're building standalone.
- # common/Makefile.Flags sets NK_CFLAGS  in Kbuild environments.
- ifndef NK_CFLAGS
--STATICHEADERS += ${SOURCE_ROOT}/configs/$(PLAT)/autoconf.h
--INCLUDES += "-I${SOURCE_ROOT}/configs/$(PLAT)"
-+STATICHEADERS += ${SOURCE_ROOT}/configs/$(PLAT)/$(BOARD)/autoconf.h
-+INCLUDES += "-I${SOURCE_ROOT}/configs/$(PLAT)/$(BOARD)"
- DEFINES += -DHAVE_AUTOCONF
- ifdef DEBUG
- DEFINES += -DCONFIG_DEBUG_BUILD
---- src/kernel/sel4/src/plat/pc99/linker.lds
-+++ src/kernel/sel4/src/plat/pc99/linker.lds
-@@ -16,13 +16,13 @@
- #if defined(CONFIG_ARCH_IA32)
- #undef i386
- PADDR_BASE = 0x00000000;
--PADDR_LOAD = 0x00100000;
-+PADDR_LOAD = 0x00200000;
- KERNEL_BASE  = 0xe0000000;
- OUTPUT_ARCH(i386)
- OUTPUT_FORMAT(elf32-i386)
- #elif defined(CONFIG_ARCH_X86_64)
- PADDR_BASE = 0x00000000;
--PADDR_LOAD = 0x00100000;
-+PADDR_LOAD = 0x00200000;
- KERNEL_BASE = 0xffffffff80000000;
- OUTPUT_FORMAT(elf64-x86-64)
- #endif
 --- src/kernel/sel4/include/plat/pc99/plat/64/plat_mode/machine/hardware.h
 +++ src/kernel/sel4/include/plat/pc99/plat/64/plat_mode/machine/hardware.h
-@@ -19,7 +19,7 @@
-  * because they need to defined like this in linker.lds
-  */
- #define PADDR_BASE  UL_CONST(0x00000000)
--#define PADDR_LOAD  UL_CONST(0x00100000)
-+#define PADDR_LOAD  UL_CONST(0x00200000)
- /* our kernel window is 2^39 bits (2^9 * 1gb) and the virtual address
-  * range is 48 bits. Therefore our base is 2^48 - 2^39
-  */
+@@ -87,7 +87,7 @@
+ #define PPTR_TOP UL_CONST(0xffffffff80000000)
+ 
+ /* The physical memory address to use for mapping the kernel ELF */
+-#define KERNEL_ELF_PADDR_BASE UL_CONST(0x00100000)
++#define KERNEL_ELF_PADDR_BASE UL_CONST(0x00200000)
+ 
+ /* Kernel mapping starts directly after the physical memory window */
+ #define KERNEL_ELF_BASE (PPTR_TOP + KERNEL_ELF_PADDR_BASE)
 --- src/kernel/sel4/include/plat/pc99/plat/32/plat_mode/machine/hardware.h
 +++ src/kernel/sel4/include/plat/pc99/plat/32/plat_mode/machine/hardware.h
-@@ -15,7 +15,7 @@
+@@ -74,7 +74,7 @@
+ #define PPTR_TOP KS_LOG_PPTR
  
- /* WARNING: some of these constants are also defined in linker.lds */
- #define PADDR_BASE  0x00000000
--#define PADDR_LOAD  0x00100000
-+#define PADDR_LOAD  0x00200000
- #define PPTR_BASE   0xe0000000
+ /* The physical memory address to use for mapping the kernel ELF */
+-#define KERNEL_ELF_PADDR_BASE UL_CONST(0x00100000)
++#define KERNEL_ELF_PADDR_BASE UL_CONST(0x00200000)
  
- #define PPTR_USER_TOP (PPTR_BASE & (~MASK(seL4_LargePageBits)))
+ /* The base address in virtual memory to use for the kernel ELF mapping */
+ #define KERNEL_ELF_BASE (PPTR_BASE + KERNEL_ELF_PADDR_BASE)
diff --git a/repos/base-sel4/patches/gcc12.patch b/repos/base-sel4/patches/gcc12.patch
index 408a0f0842..15ab25ddd6 100644
--- a/repos/base-sel4/patches/gcc12.patch
+++ b/repos/base-sel4/patches/gcc12.patch
@@ -1,17 +1,15 @@
 gcc12.patch
 
-diff --git src/kernel/sel4/src/arch/x86/kernel/cmdline.c src/kernel/sel4/src/arch/x86/kernel/cmdline.c
-index 6ba5d8668..0459297fa 100644
 --- src/kernel/sel4/src/arch/x86/kernel/cmdline.c
 +++ src/kernel/sel4/src/arch/x86/kernel/cmdline.c
-@@ -112,14 +112,20 @@ void cmdline_parse(const char *cmdline, cmdline_opt_t* cmdline_opt)
+@@ -109,14 +109,20 @@
      /* use BIOS data area to read serial configuration. The BDA is not
       * fully standardized and parts are absolete. See http://wiki.osdev.org/Memory_Map_(x86)#BIOS_Data_Area_.28BDA.29
       * for an explanation */
 +#pragma GCC diagnostic push
 +#pragma GCC diagnostic ignored "-Warray-bounds"
-     const unsigned short * bda_port = (unsigned short *)0x400;
-     const unsigned short * bda_equi = (unsigned short *)0x410;
+     const unsigned short *bda_port = (unsigned short *)0x400;
+     const unsigned short *bda_equi = (unsigned short *)0x410;
      int const bda_ports_count       = (*bda_equi >> 9) & 0x7;
 +#pragma GCC diagnostic pop
  #endif
@@ -25,7 +23,7 @@ index 6ba5d8668..0459297fa 100644
  
      if (parse_opt(cmdline, "console_port", cmdline_val, MAX_CMDLINE_VAL_LEN) != -1) {
          parse_uint16_array(cmdline_val, &cmdline_opt->console_port, 1);
-@@ -141,7 +147,10 @@ void cmdline_parse(const char *cmdline, cmdline_opt_t* cmdline_opt)
+@@ -138,7 +144,10 @@
  
  #ifdef CONFIG_DEBUG_BUILD
      /* initialise to default or use BDA if available */
@@ -36,16 +34,14 @@ index 6ba5d8668..0459297fa 100644
      if (parse_opt(cmdline, "debug_port", cmdline_val, MAX_CMDLINE_VAL_LEN) != -1) {
          parse_uint16_array(cmdline_val, &cmdline_opt->debug_port, 1);
      }
-diff --git src/kernel/sel4/tools/circular_includes.py src/kernel/sel4/tools/circular_includes.py
-index 825a44a5e..dc4904939 100755
 --- src/kernel/sel4/tools/circular_includes.py
 +++ src/kernel/sel4/tools/circular_includes.py
-@@ -26,7 +26,7 @@ def main():
-     resulting in the loop is printed out.
-     """
+@@ -28,7 +28,7 @@
+     if ignore_args and len(ignore_args):
+         ignore_args = [re.escape(ignore) for ignore in ignore_args]
+         ignore_re_string = '(' + '|'.join(ignore_args) + ')'
+-        ignore_re = re.compile(r'^# 1 ".*' + ignore_re_string + '"')
++        ignore_re = re.compile(r'^# [01] ".*' + ignore_re_string + '"')
  
--    kernel_all_re = re.compile(r'^# 1 ".*kernel_all\.c"')
-+    kernel_all_re = re.compile(r'^# [01] ".*kernel_all\.c"')
      header_re = re.compile(r'^# (\d+) "(.*\..)"')
  
-     file_stack = []
diff --git a/repos/base-sel4/patches/imx6q_sabrelite.config b/repos/base-sel4/patches/imx6q_sabrelite.config
deleted file mode 100644
index 3638b226ec..0000000000
--- a/repos/base-sel4/patches/imx6q_sabrelite.config
+++ /dev/null
@@ -1,27 +0,0 @@
---- src/kernel/sel4/configs/imx6/imx6q_sabrelite/autoconf.h
-+++ src/kernel/sel4/configs/imx6/imx6q_sabrelite/autoconf.h
-@@ -41,6 +41,7 @@
- #define CONFIG_LIBSEL4DEBUG_FUNCTION_INSTRUMENTATION_NONE 1
- #define CONFIG_LIB_SEL4_UTILS 1
- #define CONFIG_LIB_SEL4_VSPACE 1
-+#define CONFIG_PRINTING 1
- #define CONFIG_LIB_PLATSUPPORT 1
- #define CONFIG_LIB_SEL4_ALLOCMAN 1
- #define CONFIG_HAVE_LIB_SEL4_SIMPLE_DEFAULT 1
-@@ -78,7 +78,7 @@
- #define CONFIG_USER_OPTIMISATION_O2 1
- #define CONFIG_LIB_CPIO 1
- #define CONFIG_RETYPE_FAN_OUT_LIMIT 256
--#define CONFIG_ROOT_CNODE_SIZE_BITS 12
-+#define CONFIG_ROOT_CNODE_SIZE_BITS 15
- #define CONFIG_NUM_PRIORITIES 256
- #define CONFIG_TESTPRINTER_REGEX ".*"
- #define CONFIG_APP_SEL4TEST 1
-@@ -93,3 +93,7 @@
- #define CONFIG_BUILDSYS_USE_CCACHE 1
- #define CONFIG_MAX_NUM_NODES 1
- #define CONFIG_KERNEL_STACK_BITS 12
-+#define CONFIG_ENABLE_BENCHMARKS 1
-+#define CONFIG_BENCHMARK_TRACK_UTILISATION 1
-+#define CONFIG_HAVE_FPU 1
-+#define CONFIG_FPU_MAX_RESTORES_SINCE_SWITCH 64
diff --git a/repos/base-sel4/patches/imx7d_sabre.config b/repos/base-sel4/patches/imx7d_sabre.config
deleted file mode 100644
index 55095bcb6d..0000000000
--- a/repos/base-sel4/patches/imx7d_sabre.config
+++ /dev/null
@@ -1,29 +0,0 @@
---- src/kernel/sel4/configs/imx7/imx7d_sabre/autoconf.h
-+++ src/kernel/sel4/configs/imx7/imx7d_sabre/autoconf.h
-@@ -38,6 +38,7 @@
- #define CONFIG_LIBSEL4DEBUG_FUNCTION_INSTRUMENTATION_NONE 1
- #define CONFIG_LIB_SEL4_UTILS 1
- #define CONFIG_LIB_SEL4_VSPACE 1
-+#define CONFIG_PRINTING 1
- #define CONFIG_LIB_PLATSUPPORT 1
- #define CONFIG_LIB_SEL4_ALLOCMAN 1
- #define CONFIG_HAVE_LIB_SEL4_SIMPLE_DEFAULT 1
-@@ -75,7 +76,7 @@
- #define CONFIG_USER_OPTIMISATION_O2 1
- #define CONFIG_LIB_CPIO 1
- #define CONFIG_RETYPE_FAN_OUT_LIMIT 256
--#define CONFIG_ROOT_CNODE_SIZE_BITS 12
-+#define CONFIG_ROOT_CNODE_SIZE_BITS 15
- #define CONFIG_NUM_PRIORITIES 256
- #define CONFIG_TESTPRINTER_REGEX ".*"
- #define CONFIG_APP_SEL4TEST 1
-@@ -89,3 +90,9 @@
- #define CONFIG_BUILDSYS_USE_CCACHE 1
- #define CONFIG_MAX_NUM_NODES 1
- #define CONFIG_KERNEL_STACK_BITS 12
-+#define CONFIG_ARCH_AARCH32 1
-+#define CONFIG_IPC_BUF_TPIDRURW 1
-+#define CONFIG_ENABLE_BENCHMARKS 1
-+#define CONFIG_BENCHMARK_TRACK_UTILISATION 1
-+#define CONFIG_HAVE_FPU 1
-+#define CONFIG_FPU_MAX_RESTORES_SINCE_SWITCH 64
diff --git a/repos/base-sel4/patches/intel_vmcs.patch b/repos/base-sel4/patches/intel_vmcs.patch
index f0806b05a1..46250f6de3 100644
--- a/repos/base-sel4/patches/intel_vmcs.patch
+++ b/repos/base-sel4/patches/intel_vmcs.patch
@@ -1,15 +1,14 @@
 --- src/kernel/sel4/src/arch/x86/object/vcpu.c
 +++ src/kernel/sel4/src/arch/x86/object/vcpu.c
-@@ -760,6 +774,8 @@ decodeWriteVMCS(cap_t cap, word_t length, word_t* buffer)
-     case VMX_GUEST_CR3:
+@@ -713,6 +727,7 @@ static exception_t decodeWriteVMCS(cap_t cap, word_t length, word_t *buffer)
      case VMX_CONTROL_EXCEPTION_BITMAP:
      case VMX_CONTROL_ENTRY_INTERRUPTION_INFO:
-+    case VMX_CONTROL_ENTRY_EXCEPTION_ERROR_CODE:
+     case VMX_CONTROL_ENTRY_EXCEPTION_ERROR_CODE:
 +    case VMX_CONTROL_ENTRY_INSTRUCTION_LENGTH:
          break;
      case VMX_CONTROL_PIN_EXECUTION_CONTROLS:
          value = applyFixedBits(value, pin_control_high, pin_control_low);
-@@ -909,6 +925,7 @@ decodeReadVMCS(cap_t cap, word_t length, word_t* buffer)
+@@ -860,6 +875,7 @@ static exception_t decodeReadVMCS(cap_t cap, word_t length, word_t *buffer)
      case VMX_GUEST_CR0:
      case VMX_GUEST_CR3:
      case VMX_GUEST_CR4:
diff --git a/repos/base-sel4/patches/intel_vmx_full_state.patch b/repos/base-sel4/patches/intel_vmx_full_state.patch
index 1d78c44c99..c212f58d15 100644
--- a/repos/base-sel4/patches/intel_vmx_full_state.patch
+++ b/repos/base-sel4/patches/intel_vmx_full_state.patch
@@ -1,26 +1,14 @@
 --- src/kernel/sel4/src/arch/x86/object/vcpu.c
 +++ src/kernel/sel4/src/arch/x86/object/vcpu.c
-@@ -88,6 +88,9 @@ static bool_t vmx_feature_ack_on_exit;
- static vcpu_t *x86KSVPIDTable[VPID_LAST + 1];
- static vpid_t x86KSNextVPID = VPID_FIRST;
+@@ -921,6 +921,8 @@
+     vmwrite(VMX_CONTROL_ENTRY_INTERRUPTION_INFO, getSyscallArg(2, buffer));
+ }
  
-+static void
-+setMRs_vmexit(uint32_t reason, word_t qualification, tcb_t *tcb);
++static void setMRs_vmexit(uint32_t reason, word_t qualification, tcb_t *tcb);
 +
- static inline bool_t
- vmxon(paddr_t vmxon_region)
+ void vcpu_sysvmenter_reply_to_user(tcb_t *tcb)
  {
-@@ -967,10 +987,8 @@ vcpu_update_state_sysvmenter(vcpu_t *vcpu)
- void
- vcpu_sysvmenter_reply_to_user(tcb_t *tcb)
- {
--    word_t *buffer;
      vcpu_t *vcpu;
- 
--    buffer = lookupIPCBuffer(true, tcb);
-     vcpu = tcb->tcbArch.tcbVCPU;
- 
-     assert(vcpu);
 @@ -979,11 +997,9 @@ vcpu_sysvmenter_reply_to_user(tcb_t *tcb)
          switchVCPU(vcpu);
      }
@@ -35,12 +23,12 @@
  }
  
  exception_t
-@@ -1113,27 +1141,27 @@ vtx_init(void)
+@@ -1065,29 +1067,29 @@
+     return true;
  }
  
- static void
--setMRs_vmexit(uint32_t reason, word_t qualification)
-+setMRs_vmexit(uint32_t reason, word_t qualification, tcb_t *tcb)
+-static void setMRs_vmexit(uint32_t reason, word_t qualification)
++static void setMRs_vmexit(uint32_t reason, word_t qualification, tcb_t *tcb)
  {
      word_t *buffer;
      int i;
@@ -49,21 +37,23 @@
 +    buffer = lookupIPCBuffer(true, tcb);
  
 -    setMR(NODE_STATE(ksCurThread), buffer, SEL4_VMENTER_CALL_EIP_MR, vmread(VMX_GUEST_RIP));
--    setMR(NODE_STATE(ksCurThread), buffer, SEL4_VMENTER_CALL_CONTROL_PPC_MR, vmread(VMX_CONTROL_PRIMARY_PROCESSOR_CONTROLS));
+-    setMR(NODE_STATE(ksCurThread), buffer, SEL4_VMENTER_CALL_CONTROL_PPC_MR,
++    setMR(tcb, buffer, SEL4_VMENTER_CALL_EIP_MR, vmread(VMX_GUEST_RIP));
++    setMR(tcb, buffer, SEL4_VMENTER_CALL_CONTROL_PPC_MR,
+           vmread(VMX_CONTROL_PRIMARY_PROCESSOR_CONTROLS));
 -    setMR(NODE_STATE(ksCurThread), buffer, SEL4_VMENTER_CALL_CONTROL_ENTRY_MR, vmread(VMX_CONTROL_ENTRY_INTERRUPTION_INFO));
 -    setMR(NODE_STATE(ksCurThread), buffer, SEL4_VMENTER_FAULT_REASON_MR, reason);
 -    setMR(NODE_STATE(ksCurThread), buffer, SEL4_VMENTER_FAULT_QUALIFICATION_MR, qualification);
-+    setMR(tcb, buffer, SEL4_VMENTER_CALL_EIP_MR, vmread(VMX_GUEST_RIP));
-+    setMR(tcb, buffer, SEL4_VMENTER_CALL_CONTROL_PPC_MR, vmread(VMX_CONTROL_PRIMARY_PROCESSOR_CONTROLS));
-+    setMR(tcb, buffer, SEL4_VMENTER_CALL_CONTROL_ENTRY_MR, vmread(VMX_CONTROL_ENTRY_INTERRUPTION_INFO));
-+    setMR(tcb, buffer, SEL4_VMENTER_FAULT_REASON_MR, reason);
-+    setMR(tcb, buffer, SEL4_VMENTER_FAULT_QUALIFICATION_MR, qualification);
- 
+-
 -    setMR(NODE_STATE(ksCurThread), buffer, SEL4_VMENTER_FAULT_INSTRUCTION_LEN_MR, vmread(VMX_DATA_EXIT_INSTRUCTION_LENGTH));
 -    setMR(NODE_STATE(ksCurThread), buffer, SEL4_VMENTER_FAULT_GUEST_PHYSICAL_MR, vmread(VMX_DATA_GUEST_PHYSICAL));
 -    setMR(NODE_STATE(ksCurThread), buffer, SEL4_VMENTER_FAULT_RFLAGS_MR, vmread(VMX_GUEST_RFLAGS));
 -    setMR(NODE_STATE(ksCurThread), buffer, SEL4_VMENTER_FAULT_GUEST_INT_MR, vmread(VMX_GUEST_INTERRUPTABILITY));
 -    setMR(NODE_STATE(ksCurThread), buffer, SEL4_VMENTER_FAULT_CR3_MR, vmread(VMX_GUEST_CR3));
++    setMR(tcb, buffer, SEL4_VMENTER_CALL_CONTROL_ENTRY_MR, vmread(VMX_CONTROL_ENTRY_INTERRUPTION_INFO));
++    setMR(tcb, buffer, SEL4_VMENTER_FAULT_REASON_MR, reason);
++    setMR(tcb, buffer, SEL4_VMENTER_FAULT_QUALIFICATION_MR, qualification);
++
 +    setMR(tcb, buffer, SEL4_VMENTER_FAULT_INSTRUCTION_LEN_MR, vmread(VMX_DATA_EXIT_INSTRUCTION_LENGTH));
 +    setMR(tcb, buffer, SEL4_VMENTER_FAULT_GUEST_PHYSICAL_MR, vmread(VMX_DATA_GUEST_PHYSICAL));
 +    setMR(tcb, buffer, SEL4_VMENTER_FAULT_RFLAGS_MR, vmread(VMX_GUEST_RFLAGS));
@@ -71,8 +61,10 @@
 +    setMR(tcb, buffer, SEL4_VMENTER_FAULT_CR3_MR, vmread(VMX_GUEST_CR3));
  
      for (i = 0; i < n_vcpu_gp_register; i++) {
--        setMR(NODE_STATE(ksCurThread), buffer, SEL4_VMENTER_FAULT_EAX + i, NODE_STATE(ksCurThread)->tcbArch.tcbVCPU->gp_registers[i]);
-+        setMR(tcb, buffer, SEL4_VMENTER_FAULT_EAX + i, tcb->tcbArch.tcbVCPU->gp_registers[i]);
+-        setMR(NODE_STATE(ksCurThread), buffer, SEL4_VMENTER_FAULT_EAX + i,
+-              NODE_STATE(ksCurThread)->tcbArch.tcbVCPU->gp_registers[i]);
++        setMR(tcb, buffer, SEL4_VMENTER_FAULT_EAX + i,
++              tcb->tcbArch.tcbVCPU->gp_registers[i]);
      }
  }
  
diff --git a/repos/base-sel4/patches/intel_vtx_check.patch b/repos/base-sel4/patches/intel_vtx_check.patch
index 3ad6455a28..690f953f4e 100644
--- a/repos/base-sel4/patches/intel_vtx_check.patch
+++ b/repos/base-sel4/patches/intel_vtx_check.patch
@@ -36,15 +36,14 @@
      case seL4_X86_EPTPML4Object:
 --- src/kernel/sel4/src/arch/x86/object/vcpu.c
 +++ src/kernel/sel4/src/arch/x86/object/vcpu.c
-@@ -409,9 +416,14 @@ applyFixedBits(uint32_t original, uint32_t high, uint32_t low)
+@@ -401,8 +401,13 @@
      return original;
  }
  
--void
+-void vcpu_init(vcpu_t *vcpu)
 +static bool_t vcpu_support_available = false;
 +
-+bool_t
- vcpu_init(vcpu_t *vcpu)
++bool_t vcpu_init(vcpu_t *vcpu)
  {
 +    if (!vcpu_support_available)
 +        return false;
@@ -61,6 +60,14 @@
  }
  
  static void
+@@ -937,6 +937,7 @@
+ 
+     buffer = lookupIPCBuffer(true, tcb);
+     vcpu = tcb->tcbArch.tcbVCPU;
++    (void)buffer;
+ 
+     assert(vcpu);
+ 
 @@ -1067,6 +1081,12 @@ vtx_init(void)
              printf("vt-x: lack of required features\n");
              return false;
diff --git a/repos/base-sel4/patches/noise.patch b/repos/base-sel4/patches/noise.patch
index 6ee65e7b6a..cdbb1f4d6b 100644
--- a/repos/base-sel4/patches/noise.patch
+++ b/repos/base-sel4/patches/noise.patch
@@ -9,101 +9,3 @@
          return;
  
      default:
---- src/kernel/sel4/libsel4/include/sel4/shared_types.h
-+++ src/kernel/sel4/libsel4/include/sel4/shared_types.h
-@@ -33,7 +33,7 @@
-     seL4_CapFault_GuardMismatch_GuardFound = seL4_CapFault_DepthMismatch_BitsFound,
-     seL4_CapFault_GuardMismatch_BitsFound,
-     SEL4_FORCE_LONG_ENUM(seL4_CapFault_Msg),
--} seL4_CapFault_Msg;
-+}; // seL4_CapFault_Msg;
- 
- #define seL4_ReadWrite seL4_CapRights_new(0, 1, 1)
- #define seL4_AllRights seL4_CapRights_new(1, 1, 1)
---- src/kernel/sel4/libsel4/sel4_arch_include/ia32/sel4/sel4_arch/constants.h
-+++ src/kernel/sel4/libsel4/sel4_arch_include/ia32/sel4/sel4_arch/constants.h
-@@ -83,7 +83,7 @@
-     seL4_VMFault_FSR,
-     seL4_VMFault_Length,
-     SEL4_FORCE_LONG_ENUM(seL4_VMFault_Msg),
--} seL4_VMFault_Msg;
-+}; // seL4_VMFault_Msg;
- 
- enum {
-     seL4_UnknownSyscall_EAX,
-@@ -99,7 +99,7 @@
-     seL4_UnknownSyscall_Syscall,
-     seL4_UnknownSyscall_Length,
-     SEL4_FORCE_LONG_ENUM(seL4_UnknownSyscall_Msg),
--} seL4_UnknownSyscall_Msg;
-+}; // seL4_UnknownSyscall_Msg;
- 
- enum {
-     seL4_UserException_FaultIP,
-@@ -109,7 +109,7 @@
-     seL4_UserException_Code,
-     seL4_UserException_Length,
-     SEL4_FORCE_LONG_ENUM(seL4_UserException_Msg)
--} seL4_UserException_Msg;
-+}; // seL4_UserException_Msg;
- 
- #endif /* __ASSEMBLER__ */
- #define seL4_FastMessageRegisters 2
---- src/kernel/sel4/libsel4/sel4_arch_include/x86_64/sel4/sel4_arch/constants.h
-+++ src/kernel/sel4/libsel4/sel4_arch_include/x86_64/sel4/sel4_arch/constants.h
-@@ -74,7 +74,7 @@
-     seL4_VMFault_FSR,
-     seL4_VMFault_Length,
-     SEL4_FORCE_LONG_ENUM(seL4_VMFault_Msg),
--} seL4_VMFault_Msg;
-+}; // seL4_VMFault_Msg;
- 
- enum {
-     seL4_UnknownSyscall_RAX,
-@@ -98,7 +98,7 @@
-     seL4_UnknownSyscall_Syscall,
-     seL4_UnknownSyscall_Length,
-     SEL4_FORCE_LONG_ENUM(seL4_UnknownSyscall_Msg)
--} seL4_UnknownSyscall_Msg;
-+}; // seL4_UnknownSyscall_Msg;
- 
- enum {
-     seL4_UserException_FaultIP,
-@@ -108,7 +108,7 @@
-     seL4_UserException_Code,
-     seL4_UserException_Length,
-     SEL4_FORCE_LONG_ENUM(seL4_UserException_Msg)
--} seL4_UserException_Msg;
-+}; // seL4_UserException_Msg;
- 
- #endif /* __ASSEMBLER__ */
- #define seL4_FastMessageRegisters 4
---- src/kernel/sel4/libsel4/sel4_arch_include/aarch32/sel4/sel4_arch/constants.h
-+++ src/kernel/sel4/libsel4/sel4_arch_include/aarch32/sel4/sel4_arch/constants.h
-@@ -40,7 +40,7 @@
-     /* length of an unknown syscall message */
-     seL4_UnknownSyscall_Length,
-     SEL4_FORCE_LONG_ENUM(seL4_UnknownSyscall_Msg),
--} seL4_UnknownSyscall_Msg;
-+}; // seL4_UnknownSyscall_Msg;
- 
- /* format of a user exception message */
- enum {
-@@ -52,7 +52,7 @@
-     /* length of a user exception */
-     seL4_UserException_Length,
-     SEL4_FORCE_LONG_ENUM(seL4_UserException_Msg),
--} seL4_UserException_Msg;
-+}; // seL4_UserException_Msg;
- 
- /* format of a vm fault message */
- enum {
-@@ -62,7 +62,7 @@
-     seL4_VMFault_FSR,
-     seL4_VMFault_Length,
-     SEL4_FORCE_LONG_ENUM(seL4_VMFault_Msg),
--} seL4_VMFault_Msg;
-+}; // seL4_VMFault_Msg;
- 
- #ifdef CONFIG_ARM_HYPERVISOR_SUPPORT
- enum {
diff --git a/repos/base-sel4/patches/sched_bug_x86.patch b/repos/base-sel4/patches/sched_bug_x86.patch
deleted file mode 100644
index c522888862..0000000000
--- a/repos/base-sel4/patches/sched_bug_x86.patch
+++ /dev/null
@@ -1,27 +0,0 @@
---- src/kernel/sel4/src/kernel/thread.c
-+++ src/kernel/sel4/src/kernel/thread.c
-@@ -437,8 +437,11 @@ scheduleTCB(tcb_t *tptr)
- void
- timerTick(void)
- {
--    if (likely(thread_state_get_tsType(NODE_STATE(ksCurThread)->tcbState) ==
--               ThreadState_Running)) {
-+    switch (thread_state_get_tsType(NODE_STATE(ksCurThread)->tcbState)) {
-+    case ThreadState_Running:
-+#ifdef CONFIG_VTX
-+    case ThreadState_RunningVM:
-+#endif
-         if (NODE_STATE(ksCurThread)->tcbTimeSlice > 1) {
-             NODE_STATE(ksCurThread)->tcbTimeSlice--;
-         } else {
-@@ -446,6 +449,10 @@ timerTick(void)
-             SCHED_APPEND_CURRENT_TCB;
-             rescheduleRequired();
-         }
-+        break;
-+    default:
-+        /* no tick updates */
-+        break;
-     }
- 
-     if (CONFIG_NUM_DOMAINS > 1) {
diff --git a/repos/base-sel4/patches/sel4_tlb_x86_bug.patch b/repos/base-sel4/patches/sel4_tlb_x86_bug.patch
deleted file mode 100644
index 8de41bf0e8..0000000000
--- a/repos/base-sel4/patches/sel4_tlb_x86_bug.patch
+++ /dev/null
@@ -1,25 +0,0 @@
---- src/kernel/sel4/src/arch/x86/kernel/vspace.c
-+++ src/kernel/sel4/src/arch/x86/kernel/vspace.c
-@@ -711,7 +711,6 @@ void unmapPage(vm_page_size_t page_size, asid_t asid, vptr_t vptr, void *pptr)
- {
-     findVSpaceForASID_ret_t find_ret;
-     lookupPTSlot_ret_t  lu_ret;
--    cap_t               threadRoot;
-     lookupPDSlot_ret_t  pd_ret;
-     pde_t               *pde;
- 
-@@ -756,12 +756,8 @@ void unmapPage(vm_page_size_t page_size, asid_t asid, vptr_t vptr, void *pptr)
-         break;
-     }
- 
--    /* check if page belongs to current address space */
--    threadRoot = TCB_PTR_CTE_PTR(NODE_STATE(ksCurThread), tcbVTable)->cap;
--    if (config_set(CONFIG_SUPPORT_PCID) || (isValidNativeRoot(threadRoot) && (vspace_root_t*)pptr_of_cap(threadRoot) == find_ret.vspace_root)) {
--        invalidateTranslationSingleASID(vptr, asid,
--                                        SMP_TERNARY(tlb_bitmap_get(find_ret.vspace_root), 0));
--    }
-+    invalidateTranslationSingleASID(vptr, asid,
-+                                    SMP_TERNARY(tlb_bitmap_get(find_ret.vspace_root), 0));
- }
- 
- void unmapPageTable(asid_t asid, vptr_t vaddr, pte_t* pt)
diff --git a/repos/base-sel4/patches/vcpu_nullptr_bug.patch b/repos/base-sel4/patches/vcpu_nullptr_bug.patch
deleted file mode 100644
index b90f722b48..0000000000
--- a/repos/base-sel4/patches/vcpu_nullptr_bug.patch
+++ /dev/null
@@ -1,13 +0,0 @@
-Bug detected by Genode and patch provided by Anna Lyons:
-http://sel4.systems/pipermail/devel/2018-September/002161.html
---- src/kernel/sel4/src/arch/x86/c_traps.c
-+++ src/kernel/sel4/src/arch/x86/c_traps.c
-@@ -111,7 +111,7 @@ slowpath(syscall_t syscall)
- {
- 
- #ifdef CONFIG_VTX
--    if (syscall == SysVMEnter) {
-+    if (syscall == SysVMEnter && NODE_STATE(ksCurThread)->tcbArch.tcbVCPU) {
-         vcpu_update_state_sysvmenter(NODE_STATE(ksCurThread)->tcbArch.tcbVCPU);
-         if (NODE_STATE(ksCurThread)->tcbBoundNotification && notification_ptr_get_state(NODE_STATE(ksCurThread)->tcbBoundNotification) == NtfnState_Active) {
-             completeSignal(NODE_STATE(ksCurThread)->tcbBoundNotification, NODE_STATE(ksCurThread));
diff --git a/repos/base-sel4/ports/sel4.hash b/repos/base-sel4/ports/sel4.hash
index 38c6fedbc3..21ef42f0bd 100644
--- a/repos/base-sel4/ports/sel4.hash
+++ b/repos/base-sel4/ports/sel4.hash
@@ -1 +1 @@
-6879db476617c80bbf3467d6b02db11608688c9b
+4cbe95411a514cec9492e32455db68d8c82b9766
diff --git a/repos/base-sel4/ports/sel4.port b/repos/base-sel4/ports/sel4.port
index 5e969b66eb..94b95b62f6 100644
--- a/repos/base-sel4/ports/sel4.port
+++ b/repos/base-sel4/ports/sel4.port
@@ -3,31 +3,19 @@ VERSION   := git
 DOWNLOADS := sel4.git
 
 URL(sel4) := https://github.com/seL4/seL4.git
-# master branch, version 9.0.1
-REV(sel4) := 0dd40b6c43a290173ea7782b97afbbbddfa23b36
+# master branch, version 12.1.0
+REV(sel4) := 21c1a2ca7a9786d1297e1ff0a132bc57eeb55530
 DIR(sel4) := src/kernel/sel4
 
+$(call check_tool,cmake)
+$(call check_tool,ninja)
 $(call check_tool,python)
 $(call check_python_module,future)
-$(call check_python_module,tempita)
+$(call check_python_module,jinja2)
 $(call check_python_module,ply)
 $(call check_python_module,six)
+# required for ARM
+$(call check_python_module,pyfdt)
+$(call check_python_module,jsonschema)
 
 PATCHES   := $(sort $(wildcard $(REP_DIR)/patches/*.patch))
-
-HASH_INPUT += $(REP_DIR)/patches/imx6q_sabrelite.config
-HASH_INPUT += $(REP_DIR)/patches/imx7d_sabre.config
-
-# adjust kernel config usable on qemu and on native hw, and add a 32bit version
-default: $(DOWNLOADS)
-	$(VERBOSE)mkdir -p src/kernel/sel4/configs/pc99/x86_64
-	$(VERBOSE)mkdir -p src/kernel/sel4/configs/pc99/ia32
-	$(VERBOSE)cp src/kernel/sel4/configs/pc99/autoconf.h src/kernel/sel4/configs/pc99/x86_64/autoconf.h
-	$(VERBOSE)mv src/kernel/sel4/configs/pc99/autoconf.h src/kernel/sel4/configs/pc99/ia32/autoconf.h
-	$(VERBOSE)sed -i "s.^ \*/. \*/\n#ifndef ARCH_IA32\n#define ARCH_IA32\n#endif\n." src/kernel/sel4/configs/pc99/ia32/autoconf.h
-	$(VERBOSE)mkdir -p src/kernel/sel4/configs/imx6/imx6q_sabrelite
-	$(VERBOSE)mv src/kernel/sel4/configs/imx6/autoconf.h src/kernel/sel4/configs/imx6/imx6q_sabrelite/autoconf.h
-	$(VERBOSE)patch -p0 <$(REP_DIR)/patches/imx6q_sabrelite.config
-	$(VERBOSE)mkdir -p src/kernel/sel4/configs/imx7/imx7d_sabre
-	$(VERBOSE)mv src/kernel/sel4/configs/imx7/autoconf.h src/kernel/sel4/configs/imx7/imx7d_sabre/autoconf.h
-	$(VERBOSE)patch -p0 <$(REP_DIR)/patches/imx7d_sabre.config
diff --git a/repos/base-sel4/recipes/src/base-sel4-x86/content.mk b/repos/base-sel4/recipes/src/base-sel4-x86/content.mk
index cca289d09e..3b7fca0e97 100644
--- a/repos/base-sel4/recipes/src/base-sel4-x86/content.mk
+++ b/repos/base-sel4/recipes/src/base-sel4-x86/content.mk
@@ -23,9 +23,7 @@ etc/board.conf:
 	echo "BOARD = pc" > etc/board.conf
 
 content:
-	for spec in x86_32 x86_64 arm; do \
-	  mv lib/mk/spec/$$spec/ld-sel4.mk lib/mk/spec/$$spec/ld.mk; \
-	  done;
+	mv lib/mk/spec/x86_64/ld-sel4.mk lib/mk/spec/x86_64/ld.mk;
 	sed -i "s/pit_timer_drv/timer/" src/timer/pit/target.inc
 	find lib/mk/spec -name kernel-sel4-*.mk -o -name syscall-sel4-*.mk |\
 		grep -v "sel4-pc.mk" | xargs rm -rf
diff --git a/repos/base-sel4/src/core/core_log_out.cc b/repos/base-sel4/src/core/core_log_out.cc
index dd3003f4c4..138bc96d0e 100644
--- a/repos/base-sel4/src/core/core_log_out.cc
+++ b/repos/base-sel4/src/core/core_log_out.cc
@@ -15,7 +15,6 @@
 #include <core_log.h>
 
 /* seL4 includes */
-#include <sel4/arch/functions.h>
-#include <sel4/arch/syscalls.h>
+#include <base/internal/sel4.h>
 
 void Core::Core_log::out(char const c) { seL4_DebugPutChar(c); }
diff --git a/repos/base-sel4/src/core/include/core_cspace.h b/repos/base-sel4/src/core/include/core_cspace.h
index cef8599382..0e6802e0ee 100644
--- a/repos/base-sel4/src/core/include/core_cspace.h
+++ b/repos/base-sel4/src/core/include/core_cspace.h
@@ -35,12 +35,13 @@ class Core::Core_cspace
 
 		/* selectors for initially created CNodes during core bootup */
 		static unsigned top_cnode_sel()       { return (unsigned)sel4_boot_info().empty.start; }
-		static unsigned core_pad_cnode_sel()  { return top_cnode_sel() + 1; }
+		static unsigned core_pad_cnode_sel()  { return top_cnode_sel()      + 1; }
 		static unsigned core_cnode_sel()      { return core_pad_cnode_sel() + 1; }
-		static unsigned phys_cnode_sel()      { return core_cnode_sel() + 1; }
-		static unsigned untyped_cnode_4k()    { return phys_cnode_sel() + 1; }
-		static unsigned untyped_cnode_16k()   { return untyped_cnode_4k() + 1; }
-		static unsigned core_static_sel_end() { return untyped_cnode_16k() + 1; }
+		static unsigned phys_cnode_sel()      { return core_cnode_sel()     + 1; }
+		static unsigned untyped_cnode_4k()    { return phys_cnode_sel()     + 1; }
+		static unsigned untyped_cnode_16k()   { return untyped_cnode_4k()   + 1; }
+		static unsigned io_port_sel()         { return untyped_cnode_16k()  + 1; }
+		static unsigned core_static_sel_end() { return io_port_sel()        + 1; }
 
 		/* indices within top-level CNode */
 		enum Top_cnode_idx {
diff --git a/repos/base-sel4/src/core/include/initial_untyped_pool.h b/repos/base-sel4/src/core/include/initial_untyped_pool.h
index 1ca7d10088..5d49f02326 100644
--- a/repos/base-sel4/src/core/include/initial_untyped_pool.h
+++ b/repos/base-sel4/src/core/include/initial_untyped_pool.h
@@ -206,9 +206,6 @@ class Core::Initial_untyped_pool
 					size_t const retype_size_limit = get_page_size()*256;
 					size_t const batch_size        = min(min(remaining_size, retype_size_limit), max_memory);
 
-					/* mark consumed untyped memory range as allocated */
-					range.free_offset += batch_size;
-
 					addr_t const phys_addr = range.phys + page_aligned_free_offset;
 					size_t const num_pages = batch_size / (1UL << size_log2);
 
@@ -228,6 +225,13 @@ class Core::Initial_untyped_pool
 						return;
 					}
 
+					/* invoke callback about the range */
+					bool const used = func(phys_addr, num_pages << size_log2,
+					                       range.device);
+
+					if (!used)
+						return;
+
 					long const ret = seL4_Untyped_Retype(service,
 					                                     type,
 					                                     size_bits,
@@ -243,6 +247,9 @@ class Core::Initial_untyped_pool
 						return;
 					}
 
+					/* mark consumed untyped memory range as allocated */
+					range.free_offset += batch_size;
+
 					/* track memory left to be converted */
 					max_memory -= batch_size;
 
@@ -251,9 +258,6 @@ class Core::Initial_untyped_pool
 						size_t const num_pages = batch_size >> get_page_size_log2();
 						Untyped_memory::convert_to_page_frames(phys_addr, num_pages);
 					}
-
-					/* invoke callback about the range */
-					func(phys_addr, num_pages << size_log2, range.device);
 				}
 			});
 		}
diff --git a/repos/base-sel4/src/core/include/platform.h b/repos/base-sel4/src/core/include/platform.h
index fadbf6747c..4d8c8e2511 100644
--- a/repos/base-sel4/src/core/include/platform.h
+++ b/repos/base-sel4/src/core/include/platform.h
@@ -225,6 +225,11 @@ class Core::Platform : public Platform_generic
 		 */
 		long _unmap_page_frame(Cap_sel const &);
 
+		/**
+		 * Initialize I/O ports on x86
+		 */
+		void _init_io_ports();
+
 	public:
 
 		/**
diff --git a/repos/base-sel4/src/core/include/platform_thread.h b/repos/base-sel4/src/core/include/platform_thread.h
index 50df72e582..13a5000529 100644
--- a/repos/base-sel4/src/core/include/platform_thread.h
+++ b/repos/base-sel4/src/core/include/platform_thread.h
@@ -50,8 +50,8 @@ class Core::Platform_thread : public List<Platform_thread>::Element
 		/**
 		 * Virtual address of the IPC buffer within the PDs address space
 		 *
-		 * The value is 0 for the PD's main thread. For all other threads,
-		 * the value is somewhere within the stack area.
+		 * The value for the PD's main thread is INITIAL_IPC_BUFFER_VIRT.
+		 * For all other threads, the value is somewhere within the stack area.
 		 */
 		addr_t const _utcb;
 
@@ -79,6 +79,8 @@ class Core::Platform_thread : public List<Platform_thread>::Element
 		Affinity::Location _location;
 		uint16_t           _priority;
 
+		bool main_thread() const { return _utcb == INITIAL_IPC_BUFFER_VIRT; }
+
 	public:
 
 		/**
diff --git a/repos/base-sel4/src/core/include/sel4_boot_info.h b/repos/base-sel4/src/core/include/sel4_boot_info.h
index 3cd30e6f77..11c8dae114 100644
--- a/repos/base-sel4/src/core/include/sel4_boot_info.h
+++ b/repos/base-sel4/src/core/include/sel4_boot_info.h
@@ -15,7 +15,7 @@
 #define _CORE__INCLUDE__SEL4_BOOT_INFO_H_
 
 /* seL4 includes */
-#include <sel4/bootinfo.h>
+#include <base/internal/sel4.h>
 
 /* core includes */
 #include <types.h>
diff --git a/repos/base-sel4/src/core/include/thread_sel4.h b/repos/base-sel4/src/core/include/thread_sel4.h
index ac02fb7a09..6f2db0ca03 100644
--- a/repos/base-sel4/src/core/include/thread_sel4.h
+++ b/repos/base-sel4/src/core/include/thread_sel4.h
@@ -33,7 +33,8 @@ namespace Core {
 	 * Set register values for the instruction pointer and stack pointer and
 	 * start the seL4 thread
 	 */
-	void start_sel4_thread(Cap_sel tcb_sel, addr_t ip, addr_t sp, unsigned cpu);
+	void start_sel4_thread(Cap_sel tcb_sel, addr_t ip, addr_t sp, unsigned cpu,
+	                       addr_t tls_ipcbuffer);
 	void affinity_sel4_thread(Cap_sel const &tcb_sel, unsigned cpu);
 }
 
diff --git a/repos/base-sel4/src/core/include/untyped_memory.h b/repos/base-sel4/src/core/include/untyped_memory.h
index 2f811ff56b..53c916d1b4 100644
--- a/repos/base-sel4/src/core/include/untyped_memory.h
+++ b/repos/base-sel4/src/core/include/untyped_memory.h
@@ -122,8 +122,10 @@ struct Core::Untyped_memory
 			                                     num_objects);
 
 			if (ret != seL4_NoError) {
-				error(__FUNCTION__, ": seL4_Untyped_RetypeAtOffset (IA32_4K) "
-				      "returned ", ret);
+				error(__FUNCTION__, ": seL4_Untyped_RetypeAtOffset "
+				      "returned ", ret, " - physical_range=",
+				      Hex_range(node_offset << get_page_size_log2(),
+				                (num_pages - i) * get_page_size()));
 				return;
 			}
 		}
diff --git a/repos/base-sel4/src/core/platform.cc b/repos/base-sel4/src/core/platform.cc
index 31ccb0dc50..10990f30e1 100644
--- a/repos/base-sel4/src/core/platform.cc
+++ b/repos/base-sel4/src/core/platform.cc
@@ -103,18 +103,20 @@ void Platform::_init_allocators()
 
 	/* turn remaining untyped memory ranges into untyped pages */
 	_initial_untyped_pool.turn_into_untyped_object(Core_cspace::TOP_CNODE_UNTYPED_4K,
-		[&] (addr_t const phys, addr_t const size, bool const device) {
+		[&] (addr_t const phys, addr_t const size, bool const device_memory) {
 			/* register to physical or iomem memory allocator */
 
 			addr_t const phys_addr = trunc_page(phys);
 			size_t const phys_size = round_page(phys - phys_addr + size);
 
-			if (device)
+			if (device_memory)
 				_io_mem_alloc.add_range(phys_addr, phys_size);
 			else
 				_core_mem_alloc.phys_alloc().add_range(phys_addr, phys_size);
 
 			_unused_phys_alloc.remove_range(phys_addr, phys_size);
+
+			return true; /* range used by this functor */
 		});
 
 	/*
@@ -174,7 +176,7 @@ void Platform::_switch_to_core_cspace()
 	_core_cnode.copy(initial_cspace, Cnode_index(seL4_CapASIDControl));
 	_core_cnode.copy(initial_cspace, Cnode_index(seL4_CapInitThreadASIDPool));
 	/* XXX io port not available on ARM, causes just a kernel warning XXX */
-	_core_cnode.copy(initial_cspace, Cnode_index(seL4_CapIOPort));
+	_core_cnode.move(initial_cspace, Cnode_index(seL4_CapIOPortControl));
 	_core_cnode.copy(initial_cspace, Cnode_index(seL4_CapBootInfoFrame));
 	_core_cnode.copy(initial_cspace, Cnode_index(seL4_CapInitThreadIPCBuffer));
 	_core_cnode.copy(initial_cspace, Cnode_index(seL4_CapDomain));
@@ -648,8 +650,8 @@ Platform::Platform()
 			                                     affinity_space().height()));
 	}
 
-	/* I/O port allocator (only meaningful for x86) */
-	_io_port_alloc.add_range(0, 0x10000);
+	/* solely meaningful for x86 */
+	_init_io_ports();
 
 	_init_rom_modules();
 
diff --git a/repos/base-sel4/src/core/platform_pd.cc b/repos/base-sel4/src/core/platform_pd.cc
index e656024008..b2da145144 100644
--- a/repos/base-sel4/src/core/platform_pd.cc
+++ b/repos/base-sel4/src/core/platform_pd.cc
@@ -58,7 +58,8 @@ bool Platform_pd::bind_thread(Platform_thread &thread)
 		thread._ep_sel = alloc_sel();
 		thread._vcpu_sel = alloc_sel();
 		/* allocate asynchronous selector used for locks in the PD's CSpace */
-		thread._lock_sel = thread._utcb ? alloc_sel() : Cap_sel(INITIAL_SEL_LOCK);
+		thread._lock_sel = thread.main_thread() ? Cap_sel(INITIAL_SEL_LOCK)
+		                                        : alloc_sel();
 		thread._vcpu_notify_sel = alloc_sel();
 	} catch (Platform_pd::Sel_bit_alloc::Out_of_indices) {
 		if (thread._fault_handler_sel.value()) {
@@ -92,24 +93,21 @@ bool Platform_pd::bind_thread(Platform_thread &thread)
 	 *     to attach the UTCB as a dataspace to the stack area to make the RM
 	 *     session aware to the mapping. This code is missing.
 	 */
-	addr_t const utcb = (thread._utcb) ? thread._utcb
-	                                    : (addr_t)thread.INITIAL_IPC_BUFFER_VIRT;
-
 	Vm_space::Map_attr const attr { .cached         = true,
 	                                .write_combined = false,
 	                                .writeable      = true,
 	                                .executable     = false,
 	                                .flush_support  = true };
 	enum { ONE_PAGE = 1 };
-	_vm_space.alloc_page_tables(utcb, get_page_size());
-	_vm_space.map(thread._info.ipc_buffer_phys, utcb, ONE_PAGE, attr);
+	_vm_space.alloc_page_tables(thread._utcb, get_page_size());
+	_vm_space.map(thread._info.ipc_buffer_phys, thread._utcb, ONE_PAGE, attr);
 	return true;
 }
 
 
 void Platform_pd::unbind_thread(Platform_thread &thread)
 {
-	if (thread._utcb)
+	if (not thread.main_thread())
 		free_sel(thread._lock_sel);
 
 	free_sel(thread._fault_handler_sel);
@@ -117,10 +115,7 @@ void Platform_pd::unbind_thread(Platform_thread &thread)
 	free_sel(thread._vcpu_sel);
 	free_sel(thread._vcpu_notify_sel);
 
-	if (thread._utcb)
-		_vm_space.unmap(thread._utcb, 1);
-	else
-		_vm_space.unmap(thread.INITIAL_IPC_BUFFER_VIRT, 1);
+	_vm_space.unmap(thread._utcb, 1);
 }
 
 
diff --git a/repos/base-sel4/src/core/platform_thread.cc b/repos/base-sel4/src/core/platform_thread.cc
index bcd61b797e..4c535bde72 100644
--- a/repos/base-sel4/src/core/platform_thread.cc
+++ b/repos/base-sel4/src/core/platform_thread.cc
@@ -94,8 +94,10 @@ bool Core::install_mapping(Mapping const &mapping, unsigned long pager_object_ba
  ** Utilities to support the Platform_thread interface **
  ********************************************************/
 
-static void prepopulate_ipc_buffer(addr_t ipc_buffer_phys, Cap_sel ep_sel,
-                                   Cap_sel lock_sel)
+static void prepopulate_ipc_buffer(addr_t  const ipc_buffer_phys,
+                                   Cap_sel const ep_sel,
+                                   Cap_sel const lock_sel,
+                                   addr_t  const utcb_virt)
 {
 	/* IPC buffer is one page */
 	size_t const page_rounded_size = get_page_size();
@@ -112,6 +114,7 @@ static void prepopulate_ipc_buffer(addr_t ipc_buffer_phys, Cap_sel ep_sel,
 			Native_utcb &utcb = *(Native_utcb *)virt_ptr;
 			utcb.ep_sel  (ep_sel  .value());
 			utcb.lock_sel(lock_sel.value());
+			utcb.ipcbuffer(utcb_virt);
 
 			/* unmap IPC buffer from core */
 			if (!unmap_local((addr_t)virt_ptr, 1)) {
@@ -161,7 +164,7 @@ int Platform_thread::start(void *ip, void *sp, unsigned int)
 	 * thread. Once started, the thread picks up this information in the
 	 * 'Thread::_thread_bootstrap' method.
 	 */
-	prepopulate_ipc_buffer(_info.ipc_buffer_phys, _ep_sel, _lock_sel);
+	prepopulate_ipc_buffer(_info.ipc_buffer_phys, _ep_sel, _lock_sel, _utcb);
 
 	/* bind thread to PD and CSpace */
 	seL4_CNode_CapData const guard_cap_data =
@@ -177,7 +180,8 @@ int Platform_thread::start(void *ip, void *sp, unsigned int)
 	                                  no_cap_data.words[0]);
 	ASSERT(ret == 0);
 
-	start_sel4_thread(_info.tcb_sel, (addr_t)ip, (addr_t)(sp), _location.xpos());
+	start_sel4_thread(_info.tcb_sel, (addr_t)ip, (addr_t)(sp), _location.xpos(),
+	                  _utcb);
 	return 0;
 }
 
@@ -215,7 +219,7 @@ Platform_thread::Platform_thread(size_t, const char *name, unsigned priority,
                                  Affinity::Location location, addr_t utcb)
 :
 	_name(name),
-	_utcb(utcb),
+	_utcb(utcb ? utcb : addr_t(INITIAL_IPC_BUFFER_VIRT)),
 	_pager_obj_sel(platform_specific().core_sel_alloc().alloc()),
 	_location(location),
 	_priority((uint16_t)(Cpu_session::scale_priority(CONFIG_NUM_PRIORITIES, priority)))
@@ -226,7 +230,7 @@ Platform_thread::Platform_thread(size_t, const char *name, unsigned priority,
 	if (_priority > 0)
 		_priority -= 1;
 
-	_info.init(_utcb ? _utcb : (addr_t)INITIAL_IPC_BUFFER_VIRT, _priority);
+	_info.init(_utcb, _priority);
 	platform_thread_registry().insert(*this);
 }
 
@@ -284,5 +288,6 @@ void Platform_thread::setup_vcpu(Cap_sel ept, Cap_sel notification)
 	_pd->cspace_cnode(_vcpu_notify_sel).copy(platform_specific().core_cnode(),
 	                                         notification, _vcpu_notify_sel);
 
-	prepopulate_ipc_buffer(_info.ipc_buffer_phys, _vcpu_sel, _vcpu_notify_sel);
+	prepopulate_ipc_buffer(_info.ipc_buffer_phys, _vcpu_sel, _vcpu_notify_sel,
+	                       _utcb);
 }
diff --git a/repos/base-sel4/src/core/spec/arm/platform.cc b/repos/base-sel4/src/core/spec/arm/platform.cc
index c61c98f4df..a2caed4f52 100644
--- a/repos/base-sel4/src/core/spec/arm/platform.cc
+++ b/repos/base-sel4/src/core/spec/arm/platform.cc
@@ -40,7 +40,15 @@ seL4_Word Untyped_memory::smallest_page_type() {
 	return seL4_ARM_SmallPageObject; }
 
 
-void Platform::init_sel4_ipc_buffer() { }
+void Platform::init_sel4_ipc_buffer()
+{
+	/*
+	 * Setup tls pointer such, that it points to the (kernel created) core
+	 * main thread IPC buffer. It is used in seL4_GetIPCBuffer().
+	 */
+	seL4_BootInfo const &bi = sel4_boot_info();
+	seL4_SetTLSBase((unsigned long)&bi.ipcBuffer);
+}
 
 
 long Platform::_unmap_page_frame(Cap_sel const &sel) {
@@ -78,9 +86,15 @@ void Platform::_init_core_page_table_registry()
 	addr_t const max_pd_mem = MAX_PROCESS_COUNT * (1UL << Page_directory_kobj::SIZE_LOG2);
 
 	_initial_untyped_pool.turn_into_untyped_object(Core_cspace::TOP_CNODE_UNTYPED_16K,
-		[&] (addr_t const phys, addr_t const size, bool) {
+		[&] (addr_t const phys, addr_t const size, bool const device_memory) {
+
+			if (device_memory)
+				return false;
+
 			phys_alloc_16k().add_range(phys, size);
 			_unused_phys_alloc.remove_range(phys, size);
+
+			return true;
 		},
 		Page_directory_kobj::SIZE_LOG2, max_pd_mem);
 
@@ -122,3 +136,8 @@ void Platform_pd::_deinit_page_directory(addr_t phys_addr) const
 
 	Untyped_memory::free_page(phys_alloc_16k(), phys_addr);
 }
+
+
+void Platform::_init_io_ports()
+{
+}
diff --git a/repos/base-sel4/src/core/spec/arm/thread.cc b/repos/base-sel4/src/core/spec/arm/thread.cc
index f7f3d8ecb9..45a8ea9082 100644
--- a/repos/base-sel4/src/core/spec/arm/thread.cc
+++ b/repos/base-sel4/src/core/spec/arm/thread.cc
@@ -15,6 +15,7 @@
  */
 
 /* base includes */
+#include <base/internal/native_utcb.h>
 #include <base/thread_state.h>
 
 /* core includes */
@@ -24,7 +25,8 @@
 using namespace Core;
 
 
-void Core::start_sel4_thread(Cap_sel tcb_sel, addr_t ip, addr_t sp, unsigned cpu)
+void Core::start_sel4_thread(Cap_sel tcb_sel, addr_t ip, addr_t sp,
+                             unsigned cpu, addr_t const virt_utcb)
 {
 	/* set register values for the instruction pointer and stack pointer */
 	seL4_UserContext regs;
@@ -40,6 +42,14 @@ void Core::start_sel4_thread(Cap_sel tcb_sel, addr_t ip, addr_t sp, unsigned cpu
 
 	affinity_sel4_thread(tcb_sel, cpu);
 
+	/*
+	 * Set tls pointer to location, where ipcbuffer address is stored, so
+	 * that it can be used by seL4_GetIPCBuffer()
+	 */
+	auto error = seL4_TCB_SetTLSBase(tcb_sel.value(),
+	                                 virt_utcb + Native_utcb::tls_ipcbuffer_offset);
+	ASSERT(not error);
+
 	seL4_TCB_Resume(tcb_sel.value());
 }
 
diff --git a/repos/base-sel4/src/core/spec/x86/io_port_session_support.cc b/repos/base-sel4/src/core/spec/x86/io_port_session_support.cc
index bc78bb165b..f1230a7965 100644
--- a/repos/base-sel4/src/core/spec/x86/io_port_session_support.cc
+++ b/repos/base-sel4/src/core/spec/x86/io_port_session_support.cc
@@ -25,7 +25,7 @@ unsigned char Io_port_session_component::inb(unsigned short address)
 	/* check boundaries */
 	if (!_in_bounds(address, sizeof(unsigned char))) return 0;
 
-	seL4_X86_IOPort_In8_t v = seL4_X86_IOPort_In8(seL4_CapIOPort, address);
+	auto const v = seL4_X86_IOPort_In8(Core_cspace::io_port_sel(), address);
 	if (v.error == seL4_NoError)
 		return v.result;
 
@@ -39,7 +39,7 @@ unsigned short Io_port_session_component::inw(unsigned short address)
 	/* check boundaries */
 	if (!_in_bounds(address, sizeof(unsigned short))) return 0;
 
-	seL4_X86_IOPort_In16_t v = seL4_X86_IOPort_In16(seL4_CapIOPort, address);
+	auto const v = seL4_X86_IOPort_In16(Core_cspace::io_port_sel(), address);
 	if (v.error == seL4_NoError)
 		return v.result;
 
@@ -53,7 +53,7 @@ unsigned Io_port_session_component::inl(unsigned short address)
 	/* check boundaries */
 	if (!_in_bounds(address, sizeof(unsigned))) return 0;
 
-	seL4_X86_IOPort_In32_t v = seL4_X86_IOPort_In32(seL4_CapIOPort, address);
+	auto const v = seL4_X86_IOPort_In32(Core_cspace::io_port_sel(), address);
 	if (v.error == seL4_NoError)
 		return v.result;
 
@@ -67,7 +67,7 @@ void Io_port_session_component::outb(unsigned short address, unsigned char value
 	/* check boundaries */
 	if (!_in_bounds(address, sizeof(unsigned char))) return;
 
-	int result = seL4_X86_IOPort_Out8(seL4_CapIOPort, address, value);
+	int result = seL4_X86_IOPort_Out8(Core_cspace::io_port_sel(), address, value);
 
 	if (result != seL4_NoError)
 		error(__PRETTY_FUNCTION__, " failed ", result);
@@ -79,7 +79,7 @@ void Io_port_session_component::outw(unsigned short address, unsigned short valu
 	/* check boundaries */
 	if (!_in_bounds(address, sizeof(unsigned short))) return;
 
-	int result = seL4_X86_IOPort_Out16(seL4_CapIOPort, address, value);
+	int result = seL4_X86_IOPort_Out16(Core_cspace::io_port_sel(), address, value);
 
 	if (result != seL4_NoError)
 		error(__PRETTY_FUNCTION__, " failed ", result);
@@ -91,7 +91,7 @@ void Io_port_session_component::outl(unsigned short address, unsigned value)
 	/* check boundaries */
 	if (!_in_bounds(address, sizeof(unsigned))) return;
 
-	int result = seL4_X86_IOPort_Out32(seL4_CapIOPort, address, value);
+	int result = seL4_X86_IOPort_Out32(Core_cspace::io_port_sel(), address, value);
 
 	if (result != seL4_NoError)
 		error(__PRETTY_FUNCTION__, " failed ", result);
diff --git a/repos/base-sel4/src/core/spec/x86_64/platform.cc b/repos/base-sel4/src/core/spec/x86_64/platform.cc
index b5228eaafe..1a2052b1d5 100644
--- a/repos/base-sel4/src/core/spec/x86_64/platform.cc
+++ b/repos/base-sel4/src/core/spec/x86_64/platform.cc
@@ -27,7 +27,15 @@ using namespace Core;
 seL4_Word Untyped_memory::smallest_page_type() { return seL4_X86_4K; }
 
 
-void Platform::init_sel4_ipc_buffer() { }
+void Platform::init_sel4_ipc_buffer()
+{
+	/*
+	 * Setup tls pointer such, that it points to the (kernel created) core
+	 * main thread IPC buffer. The fs register is used in seL4_GetIPCBuffer().
+	 */
+	seL4_BootInfo const &bi = sel4_boot_info();
+	seL4_SetTLSBase((unsigned long)&bi.ipcBuffer);
+}
 
 
 long Platform::_unmap_page_frame(Cap_sel const &sel) {
@@ -74,31 +82,37 @@ void Platform::_init_core_page_table_registry()
 	addr_t const max_pd_mem = MAX_VCPU_COUNT * (1UL << Vcpu_kobj::SIZE_LOG2);
 
 	_initial_untyped_pool.turn_into_untyped_object(Core_cspace::TOP_CNODE_UNTYPED_16K,
-		[&] (addr_t const phys, addr_t const size, bool) {
+		[&] (addr_t const phys, addr_t const size, bool const device_memory) {
+
+			if (device_memory)
+				return false;
+
 			phys_alloc_16k().add_range(phys, size);
 			_unused_phys_alloc.remove_range(phys, size);
+
+			return true;
 		},
 		Vcpu_kobj::SIZE_LOG2, max_pd_mem);
 
 	log(":phys_mem_16k:     ",  phys_alloc_16k());
-
-	/*
-	 * Register initial page frames
-	 * - actually we don't use them in core -> skip
-	 */
-#if 0
-	addr_t const modules_start = reinterpret_cast<addr_t>(&_boot_modules_binaries_begin);
-	addr_t const modules_end   = reinterpret_cast<addr_t>(&_boot_modules_binaries_end);
-
-	virt_addr = (addr_t)(&_prog_img_beg);
-	for (unsigned sel = bi.userImageFrames.start;
-	     sel < bi.userImageFrames.end;
-	     sel++, virt_addr += get_page_size()) {
-		/* skip boot modules */
-		if (modules_start <= virt_addr && virt_addr <= modules_end)
-			continue;
-
-		_core_page_table_registry.insert_page_table_entry(virt_addr, sel);
-	}
-#endif
+}
+
+
+void Platform::_init_io_ports()
+{
+	enum { PORTS = 0x10000, PORT_FIRST = 0, PORT_LAST = PORTS - 1 };
+
+	/* I/O port allocator (only meaningful for x86) */
+	_io_port_alloc.add_range(PORT_FIRST, PORTS);
+
+	/* create I/O port capability used by io_port_session_support.cc */
+	auto const root   = _core_cnode.sel().value();
+	auto const index  = Core_cspace::io_port_sel();
+	auto const depth  = CONFIG_ROOT_CNODE_SIZE_BITS;
+
+	auto const result = seL4_X86_IOPortControl_Issue(seL4_CapIOPortControl,
+	                                                 PORT_FIRST, PORT_LAST,
+	                                                 root, index, depth);
+	if (result != 0)
+		error("IO Port access not available");
 }
diff --git a/repos/base-sel4/src/core/spec/x86_64/thread.cc b/repos/base-sel4/src/core/spec/x86_64/thread.cc
index 249e423f30..3fa9a5968b 100644
--- a/repos/base-sel4/src/core/spec/x86_64/thread.cc
+++ b/repos/base-sel4/src/core/spec/x86_64/thread.cc
@@ -15,6 +15,7 @@
  */
 
 /* base includes */
+#include <base/internal/native_utcb.h>
 #include <base/thread_state.h>
 
 /* core includes */
@@ -24,7 +25,8 @@
 using namespace Core;
 
 
-void Core::start_sel4_thread(Cap_sel tcb_sel, addr_t ip, addr_t sp, unsigned cpu)
+void Core::start_sel4_thread(Cap_sel tcb_sel, addr_t ip, addr_t sp,
+                             unsigned cpu, addr_t const virt_utcb)
 {
 	/* set register values for the instruction pointer and stack pointer */
 	seL4_UserContext regs;
@@ -40,6 +42,14 @@ void Core::start_sel4_thread(Cap_sel tcb_sel, addr_t ip, addr_t sp, unsigned cpu
 
 	affinity_sel4_thread(tcb_sel, cpu);
 
+	/*
+	 * Set tls pointer to location, where ipcbuffer address is stored, so
+	 * that it can be used by register fs (seL4_GetIPCBuffer())
+	 */
+	auto error = seL4_TCB_SetTLSBase(tcb_sel.value(),
+	                                 virt_utcb + Native_utcb::tls_ipcbuffer_offset);
+	ASSERT(not error);
+
 	seL4_TCB_Resume(tcb_sel.value());
 }
 
diff --git a/repos/base-sel4/src/core/thread_start.cc b/repos/base-sel4/src/core/thread_start.cc
index c93ac873a3..cd2e34a27e 100644
--- a/repos/base-sel4/src/core/thread_start.cc
+++ b/repos/base-sel4/src/core/thread_start.cc
@@ -101,8 +101,11 @@ void Thread::_thread_start()
 
 void Thread::start()
 {
+	/* write ipcbuffer address to utcb*/
+	utcb()->ipcbuffer(addr_t(utcb()));
+
 	start_sel4_thread(Cap_sel(native_thread().tcb_sel), (addr_t)&_thread_start,
-	                  (addr_t)stack_top(), _affinity.xpos());
+	                  (addr_t)stack_top(), _affinity.xpos(), addr_t(utcb()));
 
 	struct Core_trace_source : public  Core::Trace::Source::Info_accessor,
 	                           private Core::Trace::Control,
diff --git a/repos/base-sel4/src/include/base/internal/native_utcb.h b/repos/base-sel4/src/include/base/internal/native_utcb.h
index a38f761f84..edb061ae33 100644
--- a/repos/base-sel4/src/include/base/internal/native_utcb.h
+++ b/repos/base-sel4/src/include/base/internal/native_utcb.h
@@ -35,6 +35,10 @@ struct Genode::Native_utcb
 
 	void ep_sel  (addr_t sel) { _raw[ELEMENTS - 1] = sel; }
 	void lock_sel(addr_t sel) { _raw[ELEMENTS - 2] = sel; }
+
+	static addr_t constexpr tls_ipcbuffer_offset = (ELEMENTS - 3) * sizeof(_raw[0]);
+
+	void ipcbuffer(addr_t const addr) { _raw[ELEMENTS - 3] = addr; }
 };
 
 #endif /* _INCLUDE__BASE__INTERNAL__NATIVE_UTCB_H_ */
diff --git a/repos/base-sel4/src/include/base/internal/raw_write_string.h b/repos/base-sel4/src/include/base/internal/raw_write_string.h
index b26e8b4b7c..2bc61fe66c 100644
--- a/repos/base-sel4/src/include/base/internal/raw_write_string.h
+++ b/repos/base-sel4/src/include/base/internal/raw_write_string.h
@@ -15,8 +15,7 @@
 #define _INCLUDE__BASE__INTERNAL__RAW_WRITE_STRING_H_
 
 /* seL4 includes */
-#include <sel4/arch/functions.h>
-#include <sel4/arch/syscalls.h>
+#include <base/internal/sel4.h>
 
 namespace Genode {
 
diff --git a/tool/run/boot_dir/sel4 b/tool/run/boot_dir/sel4
index 59fb26738a..b324d0d9d7 100644
--- a/tool/run/boot_dir/sel4
+++ b/tool/run/boot_dir/sel4
@@ -12,7 +12,7 @@ proc kernel_files          { } { return sel4 }
 
 proc boot_output { } { return "serial" }
 
-proc run_boot_string   { } { return "\n\rBooting all finished, dropped to user space" }
+proc run_boot_string   { } { return "\nBooting all finished, dropped to user space" }
 proc core_link_address { } { return "0x02000000" }
 
 proc sel4_elfloader_dir { } {