diff --git a/repos/base-sel4/patches/dev_mem_4k.patch b/repos/base-sel4/patches/dev_mem_4k.patch
new file mode 100644
index 0000000000..e53bd0534d
--- /dev/null
+++ b/repos/base-sel4/patches/dev_mem_4k.patch
@@ -0,0 +1,11 @@
+--- src/kernel/sel4/src/arch/x86/kernel/boot.c
++++ src/kernel/sel4/src/arch/x86/kernel/boot.c
+@@ -83,7 +83,7 @@ create_device_frames(
+         /* use large frames if possible, otherwise use 4K frames */
+         if (IS_ALIGNED(dev_reg.start, LARGE_PAGE_BITS) &&
+                 IS_ALIGNED(dev_reg.end,   LARGE_PAGE_BITS)) {
+-            frame_size = X86_LargePage;
++            frame_size = X86_SmallPage;
+         } else {
+             frame_size = X86_SmallPage;
+         }
diff --git a/repos/base-sel4/ports/sel4.hash b/repos/base-sel4/ports/sel4.hash
index bb88136d80..27c605babf 100644
--- a/repos/base-sel4/ports/sel4.hash
+++ b/repos/base-sel4/ports/sel4.hash
@@ -1 +1 @@
-4a35ff120456dea8de73ace7d9af53ace91da540
+c8947bc79b1c29d570be6ad917c8310bc79d39e1
diff --git a/repos/base-sel4/src/core/platform.cc b/repos/base-sel4/src/core/platform.cc
index 9f601f4975..6a761ea044 100644
--- a/repos/base-sel4/src/core/platform.cc
+++ b/repos/base-sel4/src/core/platform.cc
@@ -144,6 +144,11 @@ void Platform::_init_allocators()
 
 	for (unsigned region = 0; region < bi.numDeviceRegions; region++) {
 		size_t const frame_size = 1UL << bi.deviceRegions[region].frameSizeBits;
+		if (frame_size != 4096) {
+			error("unsupported device memory frame size of ", Hex(frame_size));
+			class Unsupported_dev_memory_framesize{};
+			throw Unsupported_dev_memory_framesize();
+		}
 
 		for (uint64_t sel = bi.deviceRegions[region].frames.start,
 		     phys_addr = bi.deviceRegions[region].basePaddr;