diff --git a/headers/private/kernel/arch/x86/32/descriptors.h b/headers/private/kernel/arch/x86/32/descriptors.h
index 5308ce0547..535c6a1d5f 100644
--- a/headers/private/kernel/arch/x86/32/descriptors.h
+++ b/headers/private/kernel/arch/x86/32/descriptors.h
@@ -16,6 +16,8 @@
 #define USER_CODE_SEGMENT			3
 #define USER_DATA_SEGMENT			4
 
+#define BOOT_GDT_SEGMENT_COUNT		(USER_DATA_SEGMENT + 1)
+
 #define APM_CODE32_SEGMENT			5
 #define APM_CODE16_SEGMENT			6
 #define APM_DATA_SEGMENT			7
diff --git a/headers/private/kernel/arch/x86/64/descriptors.h b/headers/private/kernel/arch/x86/64/descriptors.h
index c5a783a611..e359741d63 100644
--- a/headers/private/kernel/arch/x86/64/descriptors.h
+++ b/headers/private/kernel/arch/x86/64/descriptors.h
@@ -13,6 +13,8 @@
 #define USER_DATA_SEGMENT		3
 #define USER_CODE_SEGMENT		4
 
+#define BOOT_GDT_SEGMENT_COUNT	(USER_CODE_SEGMENT + 1)
+
 #define KERNEL_CODE_SELECTOR	((KERNEL_CODE_SEGMENT << 3) | DPL_KERNEL)
 #define KERNEL_DATA_SELECTOR	((KERNEL_DATA_SEGMENT << 3) | DPL_KERNEL)
 
diff --git a/src/system/boot/platform/bios_ia32/long.cpp b/src/system/boot/platform/bios_ia32/long.cpp
index e558bae6f8..2152f99213 100644
--- a/src/system/boot/platform/bios_ia32/long.cpp
+++ b/src/system/boot/platform/bios_ia32/long.cpp
@@ -62,6 +62,11 @@ fix_address(FixedWidthPointer<Type>& p)
 static void
 long_gdt_init()
 {
+	STATIC_ASSERT(BOOT_GDT_SEGMENT_COUNT > KERNEL_CODE_SEGMENT
+		&& BOOT_GDT_SEGMENT_COUNT > KERNEL_DATA_SEGMENT
+		&& BOOT_GDT_SEGMENT_COUNT > USER_CODE_SEGMENT
+		&& BOOT_GDT_SEGMENT_COUNT > USER_DATA_SEGMENT);
+
 	clear_segment_descriptor(&gBootGDT[0]);
 
 	// Set up code/data segments (TSS segments set up later in the kernel).
diff --git a/src/system/boot/platform/bios_ia32/mmu.cpp b/src/system/boot/platform/bios_ia32/mmu.cpp
index e70929fb91..8cf746f565 100644
--- a/src/system/boot/platform/bios_ia32/mmu.cpp
+++ b/src/system/boot/platform/bios_ia32/mmu.cpp
@@ -538,6 +538,11 @@ mmu_init_for_kernel(void)
 {
 	TRACE("mmu_init_for_kernel\n");
 
+	STATIC_ASSERT(BOOT_GDT_SEGMENT_COUNT > KERNEL_CODE_SEGMENT
+		&& BOOT_GDT_SEGMENT_COUNT > KERNEL_DATA_SEGMENT
+		&& BOOT_GDT_SEGMENT_COUNT > USER_CODE_SEGMENT
+		&& BOOT_GDT_SEGMENT_COUNT > USER_DATA_SEGMENT);
+
 	// set up a new gdt
 
 	// put standard segment descriptors in GDT
diff --git a/src/system/boot/platform/bios_ia32/mmu.h b/src/system/boot/platform/bios_ia32/mmu.h
index ca373549f0..7c338a45c0 100644
--- a/src/system/boot/platform/bios_ia32/mmu.h
+++ b/src/system/boot/platform/bios_ia32/mmu.h
@@ -9,9 +9,6 @@
 #include <arch/x86/descriptors.h>
 
 
-#define BOOT_GDT_SEGMENT_COUNT	(USER_DATA_SEGMENT + 1)
-
-
 #ifndef _ASSEMBLER