diff --git a/config.cmake b/config.cmake
index e83384dbb..07a298c91 100644
--- a/config.cmake
+++ b/config.cmake
@@ -173,7 +173,7 @@ if(DEFINED KernelDTSList AND (NOT "${KernelDTSList}" STREQUAL ""))
                 --compat-strings-out "${compatibility_outfile}" --c-header --header-out
                 "${device_dest}" --hardware-config "${config_file}" --hardware-schema
                 "${config_schema}" --yaml --yaml-out "${platform_yaml}" --arch "${KernelArch}"
-                --addrspace-bits "${KernelPaddrBits}"
+                --addrspace-max "${KernelPaddrUserTop}"
             INPUT_FILE /dev/stdin
             OUTPUT_FILE /dev/stdout
             ERROR_FILE /dev/stderr
diff --git a/src/arch/arm/config.cmake b/src/arch/arm/config.cmake
index 09317c294..b49f2bffe 100644
--- a/src/arch/arm/config.cmake
+++ b/src/arch/arm/config.cmake
@@ -20,12 +20,20 @@ set(KernelArmPASizeBits40 OFF)
 set(KernelArmPASizeBits44 OFF)
 if(KernelArmCortexA53)
     set(KernelArmPASizeBits40 ON)
+    math(EXPR KernelPaddrUserTop "(1 << 40) - 1")
 elseif(KernelArmCortexA57)
     set(KernelArmPASizeBits44 ON)
+    math(EXPR KernelPaddrUserTop "(1 << 44) - 1")
 endif()
 config_set(KernelArmPASizeBits40 ARM_PA_SIZE_BITS_40 "${KernelArmPASizeBits40}")
 config_set(KernelArmPASizeBits44 ARM_PA_SIZE_BITS_44 "${KernelArmPASizeBits44}")
 
+if(KernelSel4ArchAarch32)
+    # 64-bit targets may be building in 32-bit mode,
+    # so make sure maximum paddr is 32-bit.
+    math(EXPR KernelPaddrUserTop "(1 << 32) - 1")
+endif()
+
 include(src/arch/arm/armv/armv6/config.cmake)
 include(src/arch/arm/armv/armv7-a/config.cmake)
 include(src/arch/arm/armv/armv8-a/config.cmake)
diff --git a/src/arch/riscv/config.cmake b/src/arch/riscv/config.cmake
index b466abab9..195c0734f 100644
--- a/src/arch/riscv/config.cmake
+++ b/src/arch/riscv/config.cmake
@@ -24,6 +24,21 @@ config_string(
 if(KernelSel4ArchRiscV32)
     set(KernelPTLevels 2 CACHE STRING "" FORCE)
 endif()
+if(KernelPTLevels EQUAL 2)
+    if(KernelSel4ArchRiscV32)
+        # seL4 on RISCV32 uses 32-bit ints for addresses,
+        # so limit the maximum paddr to 32-bits.
+        math(EXPR KernelPaddrUserTop "(1 << 32) - 1")
+    else()
+        math(EXPR KernelPaddrUserTop "(1 << 34) - 1")
+    endif()
+elseif(KernelPTLevels EQUAL 3)
+    # RISC-V technically supports 56-bit paddrs,
+    # but structures.bf limits us to using 39 of those bits.
+    math(EXPR KernelPaddrUserTop "(1 << 39) - 1")
+elseif(KernelPTLevels EQUAL 4)
+    math(EXPR KernelPaddrUserTop "(1 << 56) - 1")
+endif()
 
 # This is not supported on RISC-V
 set(KernelHardwareDebugAPIUnsupported ON CACHE INTERNAL "")
diff --git a/src/arch/x86/config.cmake b/src/arch/x86/config.cmake
index 3a553098d..dd5f21312 100644
--- a/src/arch/x86/config.cmake
+++ b/src/arch/x86/config.cmake
@@ -352,6 +352,9 @@ config_option(
 
 if(KernelSel4ArchIA32)
     set(KernelSetTLSBaseSelf ON)
+    math(EXPR KernelPaddrUserTop "0xffff0000")
+else()
+    math(EXPR KernelPaddrUserTop "1 << 47")
 endif()
 if(KernelSel4ArchX86_64 AND NOT KernelFSGSBaseInst)
     set(KernelSetTLSBaseSelf ON)