diff --git a/config.cmake b/config.cmake
index e1f2e8924e60ed72c8fbe2c73c5370fdb49a95b1..441641e208674921ac1bfed346658f92057964ee 100644
--- a/config.cmake
+++ b/config.cmake
@@ -45,20 +45,80 @@ set_property(
         user_data_device_C
 )
 
-#
-# Architecture selection
-#
-config_choice(
-    KernelArch
-    ARCH
-    "Architecture to use when building the kernel"
-    "arm;KernelArchARM;ARCH_ARM"
-    "riscv;KernelArchRiscV;ARCH_RISCV"
-    "x86;KernelArchX86;ARCH_X86"
-)
+# Create and set all of the Kernel config options that can
+# be derived from the seL4 arch which is one of the following:
+# aarch32, aarch64, arm_hyp, riscv32, riscv64, x86_64, ia32
+# This macro is intended to be called from within a platform config.
+macro(declare_seL4_arch sel4_arch)
+    set(KernelSel4Arch "${sel4_arch}" CACHE STRING "")
+    config_choice(
+        KernelSel4Arch
+        SEL4_ARCH
+        "Architecture mode for building the kernel"
+        "aarch32;KernelSel4ArchAarch32;ARCH_AARCH32"
+        "aarch64;KernelSel4ArchAarch64;ARCH_AARCH64"
+        "arm_hyp;KernelSel4ArchArmHyp;ARCH_ARM_HYP"
+        "riscv32;KernelSel4ArchRiscV32;ARCH_RISCV32"
+        "riscv64;KernelSel4ArchRiscV64;ARCH_RISCV64"
+        "x86_64;KernelSel4ArchX86_64;ARCH_X86_64"
+        "ia32;KernelSel4ArchIA32;ARCH_IA32"
+    )
 
-# Set defaults for common variables
-set(KernelHaveFPU OFF)
+    config_choice(
+        KernelArch
+        ARCH
+        "Architecture to use when building the kernel"
+        "arm;KernelArchARM;ARCH_ARM;KernelSel4ArchAarch32 OR KernelSel4ArchAarch64 OR KernelSel4ArchArmHyp"
+        "riscv;KernelArchRiscV;ARCH_RISCV;KernelSel4ArchRiscV32 OR KernelSel4ArchRiscV64"
+        "x86;KernelArchX86;ARCH_X86;KernelSel4ArchX86_64 OR KernelSel4ArchIA32"
+    )
+
+    # The following config options are legacy and can be removed if they
+    # aren't used anywhere anymore.
+    if(KernelArchARM)
+        config_set(KernelArmSel4Arch ARM_SEL4_ARCH "${KernelSel4Arch}")
+    elseif(KernelArchRiscV)
+        config_set(KernelRiscVSel4Arch RISCV_SEL4_ARCH "${KernelSel4Arch}")
+    elseif(KernelArchX86)
+        config_set(KernelX86Sel4Arch X86_SEL4_ARCH "${KernelSel4Arch}")
+    endif()
+
+    # arm-hyp masquerades as an aarch32 build
+    if(KernelSel4ArchArmHyp)
+        config_set(KernelSel4ArmHypAarch32 ARCH_AARCH32 ON)
+        set(KernelSel4ArchAarch32 ON CACHE INTERNAL "" FORCE)
+    else()
+        config_set(KernelSel4ArmHypAarch32 ARCH_AARCH32 OFF)
+    endif()
+
+    # Set kernel mode options
+    if(KernelSel4ArchAarch32 OR KernelSel4ArchArmHyp OR KernelSel4ArchRiscV32 OR KernelSel4ArchIA32)
+        set_kernel_32()
+    elseif(KernelSel4ArchAarch64 OR KernelSel4ArchRiscV64 OR KernelSel4ArchX86_64)
+        set_kernel_64()
+    endif()
+
+endmacro()
+
+# Register a platform's config options to be set if it is selected.
+# Additionally, the kernel_platforms variable can be used as a record of all
+# platforms that can be built once the platform configuration files have been
+# processed.
+# name: name of the platform, KernelPlatform will be set to this.
+# config1: the CMake configuration name. Such as KernelPlatImx7.
+# config2: the C header file config name without CONFIG_. Such as PLAT_IMX7_SABRE.
+# enable_test: A CMake boolean formula that allows the option to be selected.
+#     e.g. "KernelSel4ArchAarch32", or "KernelSel4ArchX86_64 OR KernelSel4ArchIA32"
+macro(declare_platform name config1 config2 enable_test)
+    list(APPEND kernel_platforms "${name}\;${config1}\;${config2}\;${enable_test}")
+    if("${KernelPlatform}" STREQUAL ${name})
+        set(${config1} ON CACHE INTERNAL "" FORCE)
+        # Write KernelPlatform into the cache in case it is only a local variable
+        set(KernelPlatform ${KernelPlatform} CACHE STRING "")
+    else()
+        set(${config1} OFF CACHE INTERNAL "" FORCE)
+    endif()
+endmacro()
 
 function(declare_default_headers)
     cmake_parse_arguments(
@@ -96,6 +156,92 @@ function(declare_default_headers)
     include_directories(include/plat/default)
 endfunction()
 
+# For all of the common variables we set a default value here if they haven't
+# been set by a platform.
+foreach(
+    var
+    IN
+    ITEMS
+    KernelArmCortexA7
+    KernelArmCortexA8
+    KernelArmCortexA9
+    KernelArmCortexA15
+    KernelArmCortexA53
+    KernelArmCortexA57
+    KernelArm1136JF_S
+    KernelArchArmV6
+    KernelArchArmV7a
+    KernelArchArmV7ve
+    KernelArchArmV8a
+    KernelArmPASizeBits40
+    KernelArmPASizeBits44
+)
+    unset(${var} CACHE)
+    set(${var} OFF)
+endforeach()
+unset(KernelArmMach CACHE)
+unset(KernelArmMachFeatureModifiers CACHE)
+unset(KernelArmCPU CACHE)
+unset(KernelArmArmV CACHE)
+
+file(GLOB result ${CMAKE_CURRENT_LIST_DIR}/src/plat/*/config.cmake)
+list(SORT result)
+
+foreach(file ${result})
+    include("${file}")
+endforeach()
+
+config_choice(KernelPlatform PLAT "Select the platform" ${kernel_platforms})
+
+# Now enshrine all the common variables in the config
+config_set(KernelArmCortexA7 ARM_CORTEX_A7 "${KernelArmCortexA7}")
+config_set(KernelArmCortexA8 ARM_CORTEX_A8 "${KernelArmCortexA8}")
+config_set(KernelArmCortexA9 ARM_CORTEX_A9 "${KernelArmCortexA9}")
+config_set(KernelArmCortexA15 ARM_CORTEX_A15 "${KernelArmCortexA15}")
+config_set(KernelArmCortexA53 ARM_CORTEX_A53 "${KernelArmCortexA53}")
+config_set(KernelArmCortexA57 ARM_CORTEX_A57 "${KernelArmCortexA57}")
+config_set(KernelArm1136JF_S ARM1136JF_S "${KernelArm1136JF_S}")
+config_set(KernelArchArmV6 ARCH_ARM_V6 "${KernelArchArmV6}")
+config_set(KernelArchArmV7a ARCH_ARM_V7A "${KernelArchArmV7a}")
+config_set(KernelArchArmV7ve ARCH_ARM_V7VE "${KernelArchArmV7ve}")
+config_set(KernelArchArmV8a ARCH_ARM_V8A "${KernelArchArmV8a}")
+config_set(KernelArmPASizeBits40 ARM_PA_SIZE_BITS_40 "${KernelArmPASizeBits40}")
+config_set(KernelArmPASizeBits44 ARM_PA_SIZE_BITS_44 "${KernelArmPASizeBits44}")
+
+# Check for v7ve before v7a as v7ve is a superset and we want to set the
+# actual armv to that, but leave armv7a config enabled for anything that
+# checks directly against it
+if(KernelArchArmV7ve)
+    set(KernelArmArmV "armv7ve" CACHE INTERNAL "")
+elseif(KernelArchArmV7a)
+    set(KernelArmArmV "armv7-a" CACHE INTERNAL "")
+elseif(KernelArchArmV8a)
+    set(KernelArmArmV "armv8-a" CACHE INTERNAL "")
+elseif(KernelArchArmV6)
+    set(KernelArmArmV "armv6" CACHE INTERNAL "")
+endif()
+if(KernelArmCortexA7)
+    set(KernelArmCPU "cortex-a7" CACHE INTERNAL "")
+elseif(KernelArmCortexA8)
+    set(KernelArmCPU "cortex-a8" CACHE INTERNAL "")
+elseif(KernelArmCortexA9)
+    set(KernelArmCPU "cortex-a9" CACHE INTERNAL "")
+elseif(KernelArmCortexA15)
+    set(KernelArmCPU "cortex-a15" CACHE INTERNAL "")
+elseif(KernelArmCortexA53)
+    set(KernelArmCPU "cortex-a53" CACHE INTERNAL "")
+elseif(KernelArmCortexA57)
+    set(KernelArmCPU "cortex-a57" CACHE INTERNAL "")
+elseif(KernelArm1136JF_S)
+    set(KernelArmCPU "arm1136jf-s" CACHE INTERNAL "")
+endif()
+if(KernelArchARM)
+    config_set(KernelArmMach ARM_MACH "${KernelArmMach}")
+endif()
+
+# Set defaults for common variables
+set(KernelHaveFPU OFF)
+
 include(src/arch/arm/config.cmake)
 include(src/arch/riscv/config.cmake)
 include(src/arch/x86/config.cmake)
diff --git a/configs/ARM_HYP_verified.cmake b/configs/ARM_HYP_verified.cmake
index 0d2e044b2deff09be5be8b43c5d9d12104ae0171..a1ab8a2410607fc44b4ad0e06ad9e7b981c06264 100644
--- a/configs/ARM_HYP_verified.cmake
+++ b/configs/ARM_HYP_verified.cmake
@@ -10,10 +10,8 @@
 # @TAG(DATA61_GPL)
 #
 
-set(KernelARMPlatform "tk1" CACHE STRING "")
-set(KernelArch "arm" CACHE STRING "")
-set(KernelArmSel4Arch "arm_hyp" CACHE STRING "")
-set(KernelArmHypervisorSupport ON CACHE BOOL "")
+set(KernelPlatform "tk1" CACHE STRING "")
+set(KernelSel4Arch "arm_hyp" CACHE STRING "")
 set(KernelVerificationBuild ON CACHE BOOL "")
 set(KernelIPCBufferLocation "threadID_register" CACHE STRING "")
 set(KernelMaxNumNodes "1" CACHE STRING "")
diff --git a/configs/ARM_verified.cmake b/configs/ARM_verified.cmake
index aab81277fedce72bd43d8d8c7bcf3861955fa753..77b169e0178b60d7d53c98203257d02fcca88d0f 100644
--- a/configs/ARM_verified.cmake
+++ b/configs/ARM_verified.cmake
@@ -10,9 +10,7 @@
 # @TAG(DATA61_GPL)
 #
 
-set(KernelARMPlatform "sabre" CACHE STRING "")
-set(KernelArch "arm" CACHE STRING "")
-set(KernelArmSel4Arch "aarch32" CACHE STRING "")
+set(KernelPlatform "imx6" CACHE STRING "")
 set(KernelVerificationBuild ON CACHE BOOL "")
 set(KernelIPCBufferLocation "threadID_register" CACHE STRING "")
 set(KernelMaxNumNodes "1" CACHE STRING "")
diff --git a/configs/RISCV64_verified.cmake b/configs/RISCV64_verified.cmake
index 7275d5ac0dac3045e1d80614c59db2e22261591e..38fc065dc6870ad078d63de5f373229b850636ae 100644
--- a/configs/RISCV64_verified.cmake
+++ b/configs/RISCV64_verified.cmake
@@ -10,9 +10,8 @@
 # @TAG(DATA61_GPL)
 #
 
-set(KernelArch "riscv" CACHE STRING "")
-set(KernelRiscVSel4Arch "riscv64" CACHE STRING "")
-set(KernelRiscVPlatform "spike" CACHE STRING "")
+set(KernelSel4Arch "riscv64" CACHE STRING "")
+set(KernelPlatform "spike" CACHE STRING "")
 set(KernelPTLevels "3" CACHE STRING "")
 set(KernelVerificationBuild ON CACHE BOOL "")
 set(KernelMaxNumNodes "1" CACHE STRING "")
diff --git a/configs/X64_verified.cmake b/configs/X64_verified.cmake
index 04ea21b4e5bc133898a6acc5ff6c21cf2fe857da..326971c435a54d51fb3c91faa662857312a6ac7a 100644
--- a/configs/X64_verified.cmake
+++ b/configs/X64_verified.cmake
@@ -10,8 +10,8 @@
 # @TAG(DATA61_GPL)
 #
 
-set(KernelArch "x86" CACHE STRING "")
-set(KernelX86Sel4Arch "x86_64" CACHE STRING "")
+set(KernelPlatform "pc99" CACHE STRING "")
+set(KernelSel4Arch "x86_64" CACHE STRING "")
 set(KernelVerificationBuild ON CACHE BOOL "")
 set(KernelMaxNumNodes "1" CACHE STRING "")
 set(KernelOptimisation "-O2" CACHE STRING "")
diff --git a/src/arch/arm/config.cmake b/src/arch/arm/config.cmake
index 065279982b473d37add1bad8aef595be4ff0e5c1..1e59daf14d32156a18d0092eeb61e505eaf224e9 100644
--- a/src/arch/arm/config.cmake
+++ b/src/arch/arm/config.cmake
@@ -12,154 +12,10 @@
 
 cmake_minimum_required(VERSION 3.7.2)
 
-config_choice(
-    KernelArmSel4Arch
-    ARM_SEL4_ARCH
-    "Architecture mode for building the kernel"
-    "aarch32;KernelSel4ArchAarch32;ARCH_AARCH32;KernelArchARM"
-    "aarch64;KernelSel4ArchAarch64;ARCH_AARCH64;KernelArchARM"
-    "arm_hyp;KernelSel4ArchArmHyp;ARCH_ARM_HYP;KernelArchARM;KernelArmHypervisorSupport"
-)
-
-config_choice(
-    KernelARMPlatform
-    ARM_PLAT
-    "Select the platform for the architecture"
-    "sabre;KernelPlatformSabre;PLAT_SABRE;KernelSel4ArchAarch32"
-    "kzm;KernelPlatformKZM;PLAT_KZM;KernelSel4ArchAarch32"
-    "omap3;KernelPlatformOMAP3;PLAT_OMAP3;KernelSel4ArchAarch32"
-    "am335x-boneblack;KernelPlatformAM335XBoneBlack;PLAT_AM335X_BONEBLACK;KernelSel4ArchAarch32"
-    "am335x-boneblue;KernelPlatformAM335XBoneBlue;PLAT_AM335X_BONEBLUE;KernelSel4ArchAarch32"
-    "exynos4;KernelPlatformExynos4;PLAT_EXYNOS4;KernelSel4ArchAarch32"
-    "exynos5410;KernelPlatformExynos5410;PLAT_EXYNOS5410;KernelSel4ArchAarch32 OR KernelSel4ArchArmHyp"
-    "exynos5422;KernelPlatformExynos5422;PLAT_EXYNOS5422;KernelSel4ArchAarch32 OR KernelSel4ArchArmHyp"
-    "exynos5250;KernelPlatformExynos5250;PLAT_EXYNOS5250;KernelSel4ArchAarch32"
-    "apq8064;KernelPlatformAPQ8064;PLAT_APQ8064;KernelSel4ArchAarch32"
-    "wandq;KernelPlatformWandQ;PLAT_WANDQ;KernelSel4ArchAarch32"
-    "imx7sabre;KernelPlatformImx7Sabre;PLAT_IMX7_SABRE;KernelSel4ArchAarch32"
-    "zynq7000;KernelPlatformZynq7000;PLAT_ZYNQ7000;KernelSel4ArchAarch32"
-    "zynqmp;KernelPlatformZynqmp;PLAT_ZYNQMP;KernelArchARM"
-    "ultra96;KernelPlatformUltra96;PLAT_ULTRA96;KernelArchARM"
-    "allwinnera20;KernelPlatformAllwinnerA20;PLAT_ALLWINNERA20;KernelSel4ArchAarch32"
-    "tk1;KernelPlatformTK1;PLAT_TK1;KernelSel4ArchAarch32 OR KernelSel4ArchArmHyp"
-    "hikey;KernelPlatformHikey;PLAT_HIKEY;KernelArchARM"
-    "rpi3;KernelPlatformRpi3;PLAT_BCM2837;KernelArchARM"
-    "tx1;KernelPlatformTx1;PLAT_TX1;KernelSel4ArchAarch64"
-    "tx2;KernelPlatformTx2;PLAT_TX2;KernelSel4ArchAarch64"
-    "odroidc2;KernelPlatformOdroidc2;PLAT_ODROIDC2;KernelSel4ArchAarch64"
-)
-
 if(KernelArchARM)
-    config_set(KernelSel4Arch SEL4_ARCH "${KernelArmSel4Arch}")
     set_property(TARGET kernel_config_target APPEND PROPERTY TOPLEVELTYPES pde_C)
 endif()
 
-# arm-hyp masquerades as an aarch32 build
-if(KernelSel4ArchArmHyp)
-    config_set(KernelSel4ArmHypAarch32 ARCH_AARCH32 ON)
-    set(KernelSel4ArchAarch32 ON CACHE INTERNAL "")
-else()
-    config_set(KernelSel4ArmHypAarch32 ARCH_AARCH32 OFF)
-endif()
-
-if(KernelSel4ArchAarch32 OR KernelSel4ArchArmHyp)
-    set_kernel_32()
-elseif(KernelSel4ArchAarch64)
-    set_kernel_64()
-endif()
-
-# Include all the platforms. For all of the common variables we set a default value here
-# and let the platforms override them.
-foreach(
-    var
-    IN
-    ITEMS
-    KernelArmCortexA7
-    KernelArmCortexA8
-    KernelArmCortexA9
-    KernelArmCortexA15
-    KernelArmCortexA53
-    KernelArmCortexA57
-    KernelArm1136JF_S
-    KernelArchArmV6
-    KernelArchArmV7a
-    KernelArchArmV7ve
-    KernelArchArmV8a
-    KernelArmPASizeBits40
-    KernelArmPASizeBits44
-)
-    unset(${var} CACHE)
-    set(${var} OFF)
-endforeach()
-unset(KernelArmMach CACHE)
-unset(KernelArmMachFeatureModifiers CACHE)
-unset(KernelArmCPU CACHE)
-unset(KernelArmArmV CACHE)
-
-include(src/plat/allwinnerA20/config.cmake)
-include(src/plat/imx6/config.cmake)
-include(src/plat/imx7/config.cmake)
-include(src/plat/imx31/config.cmake)
-include(src/plat/omap3/config.cmake)
-include(src/plat/exynos4/config.cmake)
-include(src/plat/exynos5/config.cmake)
-include(src/plat/am335x/config.cmake)
-include(src/plat/hikey/config.cmake)
-include(src/plat/apq8064/config.cmake)
-include(src/plat/bcm2837/config.cmake)
-include(src/plat/tk1/config.cmake)
-include(src/plat/tx1/config.cmake)
-include(src/plat/tx2/config.cmake)
-include(src/plat/zynq7000/config.cmake)
-include(src/plat/zynqmp/config.cmake)
-include(src/plat/odroidc2/config.cmake)
-
-# Now enshrine all the common variables in the config
-config_set(KernelArmCortexA7 ARM_CORTEX_A7 "${KernelArmCortexA7}")
-config_set(KernelArmCortexA8 ARM_CORTEX_A8 "${KernelArmCortexA8}")
-config_set(KernelArmCortexA9 ARM_CORTEX_A9 "${KernelArmCortexA9}")
-config_set(KernelArmCortexA15 ARM_CORTEX_A15 "${KernelArmCortexA15}")
-config_set(KernelArmCortexA53 ARM_CORTEX_A53 "${KernelArmCortexA53}")
-config_set(KernelArmCortexA57 ARM_CORTEX_A57 "${KernelArmCortexA57}")
-config_set(KernelArm1136JF_S ARM1136JF_S "${KernelArm1136JF_S}")
-config_set(KernelArchArmV6 ARCH_ARM_V6 "${KernelArchArmV6}")
-config_set(KernelArchArmV7a ARCH_ARM_V7A "${KernelArchArmV7a}")
-config_set(KernelArchArmV7ve ARCH_ARM_V7VE "${KernelArchArmV7ve}")
-config_set(KernelArchArmV8a ARCH_ARM_V8A "${KernelArchArmV8a}")
-config_set(KernelArmPASizeBits40 ARM_PA_SIZE_BITS_40 "${KernelArmPASizeBits40}")
-config_set(KernelArmPASizeBits44 ARM_PA_SIZE_BITS_44 "${KernelArmPASizeBits44}")
-
-# Check for v7ve before v7a as v7ve is a superset and we want to set the
-# actual armv to that, but leave armv7a config enabled for anything that
-# checks directly against it
-if(KernelArchArmV7ve)
-    set(KernelArmArmV "armv7ve" CACHE INTERNAL "")
-elseif(KernelArchArmV7a)
-    set(KernelArmArmV "armv7-a" CACHE INTERNAL "")
-elseif(KernelArchArmV8a)
-    set(KernelArmArmV "armv8-a" CACHE INTERNAL "")
-elseif(KernelArchArmV6)
-    set(KernelArmArmV "armv6" CACHE INTERNAL "")
-endif()
-if(KernelArmCortexA7)
-    set(KernelArmCPU "cortex-a7" CACHE INTERNAL "")
-elseif(KernelArmCortexA8)
-    set(KernelArmCPU "cortex-a8" CACHE INTERNAL "")
-elseif(KernelArmCortexA9)
-    set(KernelArmCPU "cortex-a9" CACHE INTERNAL "")
-elseif(KernelArmCortexA15)
-    set(KernelArmCPU "cortex-a15" CACHE INTERNAL "")
-elseif(KernelArmCortexA53)
-    set(KernelArmCPU "cortex-a53" CACHE INTERNAL "")
-elseif(KernelArmCortexA57)
-    set(KernelArmCPU "cortex-a57" CACHE INTERNAL "")
-elseif(KernelArm1136JF_S)
-    set(KernelArmCPU "arm1136jf-s" CACHE INTERNAL "")
-endif()
-if(KernelArchARM)
-    config_set(KernelArmMach ARM_MACH "${KernelArmMach}")
-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)
@@ -213,11 +69,15 @@ config_option(
     DEFAULT OFF
     DEPENDS "KernelArchARM"
 )
-
+if(KernelSel4ArchArmHyp)
+    set(default_hyp_support ON)
+else()
+    set(default_hyp_support OFF)
+endif()
 config_option(
     KernelArmHypervisorSupport ARM_HYPERVISOR_SUPPORT
     "Build as Hypervisor. Utilise ARM virtualisation extensions to build the kernel as a hypervisor"
-    DEFAULT OFF
+    DEFAULT ${default_hyp_support}
     DEPENDS "KernelArmCortexA15 OR KernelArmCortexA57"
 )
 
diff --git a/src/arch/riscv/config.cmake b/src/arch/riscv/config.cmake
index cbce46c31295acd85e6d3e04b2def142ac3985cb..460eb430ed70431bb59b6ef05af1e515c7ac3ef7 100644
--- a/src/arch/riscv/config.cmake
+++ b/src/arch/riscv/config.cmake
@@ -12,36 +12,6 @@
 
 cmake_minimum_required(VERSION 3.7.2)
 
-config_choice(
-    KernelRiscVSel4Arch
-    RISCV_SEL4_ARCH
-    "Architecture mode for building the kernel"
-    "riscv32;KernelSel4ArchRiscV32;ARCH_RISCV32;KernelArchRiscV"
-    "riscv64;KernelSel4ArchRiscV64;ARCH_RISCV64;KernelArchRiscV"
-)
-
-config_choice(
-    KernelRiscVPlatform
-    RISCV_PLAT
-    "Select the platform for the architecture"
-    "spike;KernelPlatformSpike;PLAT_SPIKE;KernelArchRiscV"
-    "hifive;KernelPlatformHifive;PLAT_HIFIVE;KernelSel4ArchRiscV64"
-)
-
-# Include all the platforms.
-include(src/plat/spike/config.cmake)
-include(src/plat/hifive/config.cmake)
-
-if(KernelArchRiscV)
-    config_set(KernelSel4Arch SEL4_ARCH "${KernelRiscVSel4Arch}")
-endif()
-
-if(KernelSel4ArchRiscV32)
-    set_kernel_32()
-elseif(KernelSel4ArchRiscV64)
-    set_kernel_64()
-endif()
-
 config_string(
     KernelPTLevels PT_LEVELS "Number of page \
     table levels for RISC-V depends on the mode. For example there are: \
diff --git a/src/arch/x86/config.cmake b/src/arch/x86/config.cmake
index aeefbc379282bb716b83f2103ff726b501387919..5cf9201b3b8e6767421c11c6364a4018870ba545 100644
--- a/src/arch/x86/config.cmake
+++ b/src/arch/x86/config.cmake
@@ -12,35 +12,16 @@
 
 cmake_minimum_required(VERSION 3.7.2)
 
-config_choice(
-    KernelX86Sel4Arch
-    X86_SEL4_ARCH
-    "Architecture mode for building the kernel"
-    "x86_64;KernelSel4ArchX86_64;ARCH_X86_64;KernelArchX86"
-    "ia32;KernelSel4ArchIA32;ARCH_IA32;KernelArchX86"
-)
-
-# Add any top level types
-if(KernelSel4ArchX86_64)
-    set_property(TARGET kernel_config_target APPEND PROPERTY TOPLEVELTYPES pdpte_C pml4e_C)
-endif()
-
 if(KernelArchX86)
-    # Only one platform so just force it to be set
-    config_set(KernelPlatform PLAT "pc99")
-    config_set(KernelPlatPC99 PLAT_PC99 ON)
-    config_set(KernelSel4Arch SEL4_ARCH "${KernelX86Sel4Arch}")
+    set_property(TARGET kernel_config_target APPEND PROPERTY TOPLEVELTYPES pde_C)
     # x86 always has an FPU
     set(KernelHaveFPU ON)
-    set_property(TARGET kernel_config_target APPEND PROPERTY TOPLEVELTYPES pde_C)
-else()
-    config_set(KernelPlatPC99 PLAT_PC99 OFF)
+
 endif()
 
+# Add any top level types
 if(KernelSel4ArchX86_64)
-    set_kernel_64()
-elseif(KernelSel4ArchIA32)
-    set_kernel_32()
+    set_property(TARGET kernel_config_target APPEND PROPERTY TOPLEVELTYPES pdpte_C pml4e_C)
 endif()
 
 config_choice(
@@ -391,7 +372,5 @@ add_sources(DEP "KernelArchX86;KernelDebugBuild" CFILES src/arch/x86/machine/cap
 
 add_bf_source_old("KernelArchX86" "structures.bf" "include/arch/x86" "arch/object")
 
-include(src/plat/pc99/config.cmake)
-
 include(src/arch/x86/32/config.cmake)
 include(src/arch/x86/64/config.cmake)
diff --git a/src/plat/allwinnerA20/config.cmake b/src/plat/allwinnerA20/config.cmake
index 52c18d9bbefb390b613aee12916d951d99b7c0b7..85ccd601a989b8890836fb88e8c321e318a50adf 100644
--- a/src/plat/allwinnerA20/config.cmake
+++ b/src/plat/allwinnerA20/config.cmake
@@ -12,12 +12,13 @@
 
 cmake_minimum_required(VERSION 3.7.2)
 
+declare_platform(allwinnera20 KernelPlatformAllwinnerA20 PLAT_ALLWINNERA20 KernelSel4ArchAarch32)
+
 if(KernelPlatformAllwinnerA20)
+    declare_seL4_arch(aarch32)
     set(KernelArmCortexA7 ON)
     set(KernelArchArmV7a ON)
-    config_set(KernelPlatAllwinnerA20 PLAT_ALLWINNERA20 ON)
-    config_set(KernelPlatform PLAT "allwinnerA20")
-    set(KernelArmMach "allwinner" CACHE INTERNAL "")
+    config_set(KernelARMPlatform ARM_PLAT allwinnera20)
     list(APPEND KernelDTSList "tools/dts/allwinnera20.dts")
     list(APPEND KernelDTSList "src/plat/allwinnerA20/overlay-allwinnera20.dts")
 
@@ -27,11 +28,9 @@ if(KernelPlatformAllwinnerA20)
         TIMER drivers/timer/allwinner.h
         INTERRUPT_CONTROLLER arch/machine/gic_pl390.h
     )
-else()
-    config_set(KernelPlatAllwinnerA20 PLAT_ALLWINNERA20 OFF)
 endif()
 
 add_sources(
-    DEP "KernelPlatAllwinnerA20"
+    DEP "KernelPlatformAllwinnerA20"
     CFILES src/plat/allwinnerA20/machine/l2cache.c src/arch/arm/machine/gic_pl390.c
 )
diff --git a/src/plat/am335x/config.cmake b/src/plat/am335x/config.cmake
index a3974c6ea789e0ccdc1fcf40100b76ced61d99b0..06ad5f881aa1b1a24597119c6e309c4eed5df406 100644
--- a/src/plat/am335x/config.cmake
+++ b/src/plat/am335x/config.cmake
@@ -12,16 +12,37 @@
 
 cmake_minimum_required(VERSION 3.7.2)
 
-if(KernelPlatformAM335XBoneBlack OR KernelPlatformAM335XBoneBlue)
+declare_platform(am335x KernelPlatformAM335X PLAT_AM335X KernelSel4ArchAarch32)
+set(c_configs PLAT_AM335X_BONEBLACK PLAT_AM335X_BONEBLUE)
+set(cmake_configs KernelPlatformAM335XBoneBlack KernelPlatformAM335XBoneBlue)
+set(plat_lists am335x-boneblack am335x-boneblue)
+foreach(config IN LISTS cmake_configs)
+    unset(${config} CACHE)
+endforeach()
+
+if(KernelPlatformAM335X)
+    declare_seL4_arch(aarch32)
     set(KernelArmCortexA8 ON)
     set(KernelArchArmV7a ON)
-    config_set(KernelPlatform PLAT "am335x")
-    config_set(KernelPlatformAM335X PLAT_AM335X ON)
-    if(KernelPlatformAM335XBoneBlack)
-        list(APPEND KernelDTSList "tools/dts/am335x-boneblack.dts")
+    if("${KernelARMPlatform}" STREQUAL "")
+        message(
+            STATUS "Selected platform am335x supports multiple sub platforms but none were given"
+        )
+        message(STATUS "  Defaulting to am335x-boneblack")
+        set(KernelARMPlatform am335x-boneblack)
+    endif()
+    list(FIND plat_lists ${KernelARMPlatform} index)
+    if("${index}" STREQUAL "-1")
+        message(FATAL_ERROR "Which am335x platform not specified")
+    endif()
+
+    list(GET c_configs ${index} c_config)
+    list(GET cmake_configs ${index} cmake_config)
+    config_set(KernelARMPlatform ARM_PLAT ${KernelARMPlatform})
+    config_set(${cmake_config} ${c_config} ON)
+    list(APPEND KernelDTSList "tools/dts/${KernelARMPlatform}.dts")
+    if("${KernelARMPlatform}" STREQUAL "am335x-boneblack")
         list(APPEND KernelDTSList "src/plat/am335x/overlay-am335x-boneblack.dts")
-    elseif(KernelPlatformAM335XBoneBlue)
-        list(APPEND KernelDTSList "tools/dts/am335x-boneblue.dts")
     endif()
     list(APPEND KernelDTSList "src/plat/am335x/overlay-am335x.dts")
 
diff --git a/src/plat/apq8064/config.cmake b/src/plat/apq8064/config.cmake
index 88227133c91326b97508e416d5aae46965e356a1..9ac41fe9b445d17c6aa5043c6697b33af32d1670 100644
--- a/src/plat/apq8064/config.cmake
+++ b/src/plat/apq8064/config.cmake
@@ -12,11 +12,14 @@
 
 cmake_minimum_required(VERSION 3.7.2)
 
+declare_platform(apq8064 KernelPlatformAPQ8064 PLAT_APQ8064 KernelSel4ArchAarch32)
+
 if(KernelPlatformAPQ8064)
+    declare_seL4_arch(aarch32)
     set(KernelArmCortexA15 ON)
     set(KernelArchArmV7a ON)
     set(KernelArchArmV7ve ON)
-    config_set(KernelPlatform PLAT "apq8064")
+    config_set(KernelARMPlatform ARM_PLAT apq8064)
     list(APPEND KernelDTSList "tools/dts/apq8064.dts")
     list(APPEND KernelDTSList "src/plat/apq8064/overlay-apq8064.dts")
 
diff --git a/src/plat/bcm2837/config.cmake b/src/plat/bcm2837/config.cmake
index df284a119b0a5a0fdaafe3680a9f144f7c390992..ea074cc57c3363587e6ca352c805d60d8b8dd718 100644
--- a/src/plat/bcm2837/config.cmake
+++ b/src/plat/bcm2837/config.cmake
@@ -12,10 +12,23 @@
 
 cmake_minimum_required(VERSION 3.7.2)
 
+declare_platform(bcm2837 KernelPlatformRpi3 PLAT_BCM2837 KernelArchARM)
+
 if(KernelPlatformRpi3)
+    if("${KernelSel4Arch}" STREQUAL aarch32)
+        declare_seL4_arch(aarch32)
+    elseif("${KernelSel4Arch}" STREQUAL aarch64)
+        declare_seL4_arch(aarch64)
+    else()
+        message(
+            STATUS "Selected platform bcm2837 supports multiple architectures but none were given"
+        )
+        message(STATUS "  Defaulting to aarch32")
+        declare_seL4_arch(aarch32)
+    endif()
     set(KernelArmCortexA53 ON)
     set(KernelArchArmV8a ON)
-    config_set(KernelPlatform PLAT "bcm2837")
+    config_set(KernelARMPlatform ARM_PLAT rpi3)
     set(KernelArmMachFeatureModifiers "+crc" CACHE INTERNAL "")
     list(APPEND KernelDTSList "tools/dts/rpi3.dts")
     list(APPEND KernelDTSList "src/plat/bcm2837/overlay-rpi3.dts")
diff --git a/src/plat/exynos4/config.cmake b/src/plat/exynos4/config.cmake
index 352b55045d823e58e5dc266c88456cfcb69f9b91..1cc8a7883750a0ee1b2ab88d3b218d87fcd86fcb 100644
--- a/src/plat/exynos4/config.cmake
+++ b/src/plat/exynos4/config.cmake
@@ -12,10 +12,13 @@
 
 cmake_minimum_required(VERSION 3.7.2)
 
+declare_platform(exynos4 KernelPlatformExynos4 PLAT_EXYNOS4 KernelSel4ArchAarch32)
+
 if(KernelPlatformExynos4)
+    declare_seL4_arch(aarch32)
     set(KernelArmCortexA9 ON)
     set(KernelArchArmV7a ON)
-    config_set(KernelPlatform PLAT "exynos4")
+    config_set(KernelARMPlatform ARM_PLAT exynos4)
     config_set(KernelArmMach MACH "exynos")
     list(APPEND KernelDTSList "tools/dts/exynos4.dts")
     list(APPEND KernelDTSList "src/plat/exynos4/overlay-exynos4.dts")
diff --git a/src/plat/exynos5/config.cmake b/src/plat/exynos5/config.cmake
index 82222085c219fb3d2a6be328e8a1702ef74a692b..67ec5ccdb23598cbb7082dac47f691bd128803d4 100644
--- a/src/plat/exynos5/config.cmake
+++ b/src/plat/exynos5/config.cmake
@@ -12,16 +12,57 @@
 
 cmake_minimum_required(VERSION 3.7.2)
 
-if(KernelPlatformExynos5250 OR KernelPlatformExynos5410 OR KernelPlatformExynos5422)
+declare_platform(
+    exynos5
+    KernelPlatExynos5
+    PLAT_EXYNOS5
+    "KernelSel4ArchAarch32 OR KernelSel4ArchArmHyp"
+)
+
+set(cmake_configs KernelPlatformExynos5250 KernelPlatformExynos5410 KernelPlatformExynos5422)
+set(c_configs PLAT_EXYNOS5250 PLAT_EXYNOS5410 PLAT_EXYNOS5422)
+set(plat_lists exynos5250 exynos5410 exynos5422)
+foreach(config IN LISTS cmake_configs)
+    unset(${config} CACHE)
+endforeach()
+unset(KernelPlatExynos54xx CACHE)
+if(KernelPlatExynos5)
+    if("${KernelSel4Arch}" STREQUAL aarch32)
+        declare_seL4_arch(aarch32)
+    elseif("${KernelSel4Arch}" STREQUAL arm_hyp)
+        declare_seL4_arch(arm_hyp)
+    else()
+        message(
+            STATUS "Selected platform exynos5 supports multiple architectures but none were given"
+        )
+        message(STATUS "  Defaulting to aarch32")
+        declare_seL4_arch(aarch32)
+    endif()
     set(KernelArmCortexA15 ON)
     set(KernelArchArmV7ve ON)
     # v7ve is a superset of v7a, so we enable that as well
     set(KernelArchArmV7a ON)
-    config_set(KernelPlatform PLAT "exynos5")
     config_set(KernelArmMach MACH "exynos")
-    config_set(KernelPlatExynos5 PLAT_EXYNOS5 ON)
+    if("${KernelARMPlatform}" STREQUAL "")
+        message(
+            STATUS "Selected platform exynos5 supports multiple sub platforms but none were given"
+        )
+        message(STATUS "  Defaulting to exynos5250")
+        set(KernelARMPlatform exynos5250)
+    endif()
+
+    list(FIND plat_lists "${KernelARMPlatform}" index)
+    if("${index}" STREQUAL "-1")
+        message(FATAL_ERROR "Invalid exynos5 platform selected: \"${KernelARMPlatform}\"")
+    endif()
+    list(GET c_configs ${index} c_config)
+    list(GET cmake_configs ${index} cmake_config)
+    config_set(KernelARMPlatform ARM_PLAT ${KernelARMPlatform})
+    config_set(${cmake_config} ${c_config} ON)
     if(KernelPlatformExynos5410 OR KernelPlatformExynos5422)
         config_set(KernelPlatExynos54xx PLAT_EXYNOS54XX ON)
+    else()
+        config_set(KernelPlatExynos54xx PLAT_EXYNOS54XX OFF)
     endif()
 
     list(APPEND KernelDTSList "tools/dts/${KernelARMPlatform}.dts")
@@ -32,9 +73,6 @@ if(KernelPlatformExynos5250 OR KernelPlatformExynos5410 OR KernelPlatformExynos5
         TIMER drivers/timer/arm_generic.h
         INTERRUPT_CONTROLLER arch/machine/gic_pl390.h
     )
-else()
-    config_set(KernelPlatExynos5 PLAT_EXYNOS5 OFF)
-    config_set(KernelPlatExynos54xx PLAT_EXYNOS54XX OFF)
 endif()
 
 add_sources(
diff --git a/src/plat/hifive/config.cmake b/src/plat/hifive/config.cmake
index 140021245adec5b8ef43db24d93974b59c61df22..d77a0ee76a0777bed8b20e97dc02cd2c5d2fe224 100644
--- a/src/plat/hifive/config.cmake
+++ b/src/plat/hifive/config.cmake
@@ -14,12 +14,17 @@
 
 cmake_minimum_required(VERSION 3.7.2)
 
+declare_platform(hifive KernelPlatformHifive PLAT_HIFIVE KernelSel4ArchRiscV64)
+
 if(KernelPlatformHifive)
-    config_set(KernelPlatform PLAT "hifive")
+    declare_seL4_arch(riscv64)
+    config_set(KernelRiscVPlatform RISCV_PLAT "hifive")
     config_set(KernelPlatformFirstHartID FIRST_HART_ID 1)
     list(APPEND KernelDTSList "tools/dts/hifive.dts")
     declare_default_headers(
         TIMER_FREQUENCY 10000000llu PLIC_MAX_NUM_INT 53
         INTERRUPT_CONTROLLER drivers/irq/hifive.h
     )
+else()
+    unset(KernelPlatformFirstHartID CACHE)
 endif()
diff --git a/src/plat/hikey/config.cmake b/src/plat/hikey/config.cmake
index 67591134458639060efa9c7d5dff6cdeaca3d7d1..eaf89e653eab511e660a96ba1a23f516ad163c44 100644
--- a/src/plat/hikey/config.cmake
+++ b/src/plat/hikey/config.cmake
@@ -12,6 +12,34 @@
 
 cmake_minimum_required(VERSION 3.7.2)
 
+declare_platform(hikey KernelPlatformHikey PLAT_HIKEY KernelArchARM)
+
+if(KernelPlatformHikey)
+    if("${KernelSel4Arch}" STREQUAL aarch32)
+        declare_seL4_arch(aarch32)
+    elseif("${KernelSel4Arch}" STREQUAL aarch64)
+        declare_seL4_arch(aarch64)
+    else()
+        message(
+            STATUS "Selected platform hikey supports multiple architectures but none were given"
+        )
+        message(STATUS "  Defaulting to aarch32")
+        declare_seL4_arch(aarch32)
+    endif()
+    set(KernelArmCortexA53 ON)
+    set(KernelArchArmV8a ON)
+    config_set(KernelARMPlatform ARM_PLAT hikey)
+    set(KernelArmMachFeatureModifiers "+crc" CACHE INTERNAL "")
+    list(APPEND KernelDTSList "tools/dts/hikey.dts")
+    list(APPEND KernelDTSList "src/plat/hikey/overlay-hikey.dts")
+    declare_default_headers(
+        TIMER_FREQUENCY 1200000llu
+        MAX_IRQ 159
+        TIMER drivers/timer/arm_generic.h
+        INTERRUPT_CONTROLLER arch/machine/gic_pl390.h
+    )
+endif()
+
 config_string(
     KernelArmHikeyOutstandingPrefetchers ARM_HIKEY_OUTSTANDING_PREFETCHERS
     "Number of outstanding prefetch allowed \
@@ -64,21 +92,6 @@ config_option(
     DEPENDS "KernelPlatformHikey;NOT KernelDebugDisablePrefetchers"
 )
 
-if(KernelPlatformHikey)
-    set(KernelArmCortexA53 ON)
-    set(KernelArchArmV8a ON)
-    config_set(KernelPlatform PLAT "hikey")
-    set(KernelArmMachFeatureModifiers "+crc" CACHE INTERNAL "")
-    list(APPEND KernelDTSList "tools/dts/hikey.dts")
-    list(APPEND KernelDTSList "src/plat/hikey/overlay-hikey.dts")
-    declare_default_headers(
-        TIMER_FREQUENCY 1200000llu
-        MAX_IRQ 159
-        TIMER drivers/timer/arm_generic.h
-        INTERRUPT_CONTROLLER arch/machine/gic_pl390.h
-    )
-endif()
-
 add_sources(
     DEP "KernelPlatformHikey"
     CFILES src/arch/arm/machine/gic_pl390.c src/arch/arm/machine/l2c_nop.c
diff --git a/src/plat/imx31/config.cmake b/src/plat/imx31/config.cmake
index 8fda8e100ec33e243b80dffc7dd9e235c73c8028..689262f611f35aa86c00cc4e698003f7c3ee2c38 100644
--- a/src/plat/imx31/config.cmake
+++ b/src/plat/imx31/config.cmake
@@ -12,10 +12,13 @@
 
 cmake_minimum_required(VERSION 3.7.2)
 
+declare_platform(imx31 KernelPlatformKZM PLAT_KZM KernelSel4ArchAarch32)
+
 if(KernelPlatformKZM)
+    declare_seL4_arch(aarch32)
     set(KernelArm1136JF_S ON)
     set(KernelArchArmV6 ON)
-    config_set(KernelPlatform PLAT "imx31")
+    config_set(KernelARMPlatform ARM_PLAT kzm)
     set(KernelArmMach "imx" CACHE INTERNAL "")
     list(APPEND KernelDTSList "tools/dts/kzm.dts")
     list(APPEND KernelDTSList "src/plat/imx31/overlay-kzm.dts")
diff --git a/src/plat/imx6/config.cmake b/src/plat/imx6/config.cmake
index 8d405b9647852511bcbdfd0b566b9e8f50cb96ba..220a9ab287f1cf0b77628078395e375a033a340b 100644
--- a/src/plat/imx6/config.cmake
+++ b/src/plat/imx6/config.cmake
@@ -12,29 +12,40 @@
 
 cmake_minimum_required(VERSION 3.7.2)
 
-if(KernelPlatformWandQ OR KernelPlatformSabre)
+declare_platform(imx6 KernelPlatImx6 PLAT_IMX6 KernelSel4ArchAarch32)
+
+set(c_configs PLAT_SABRE PLAT_WANDQ)
+set(cmake_configs KernelPlatformSabre KernelPlatformWandQ)
+set(plat_lists sabre wandq)
+foreach(config IN LISTS cmake_configs)
+    unset(${config} CACHE)
+endforeach()
+if(KernelPlatImx6)
+    declare_seL4_arch(aarch32)
     set(KernelArmCortexA9 ON)
     set(KernelArchArmV7a ON)
-    config_set(KernelPlatImx6 PLAT_IMX6 ON)
-    config_set(KernelPlatform PLAT "imx6")
     set(KernelArmMach "imx" CACHE INTERNAL "")
-
-    if(KernelPlatformWandQ)
-        list(APPEND KernelDTSList "tools/dts/wandq.dts")
-        list(APPEND KernelDTSList "src/plat/imx6/overlay-wandq.dts")
-    else()
-        list(APPEND KernelDTSList "tools/dts/sabre.dts")
-        list(APPEND KernelDTSList "src/plat/imx6/overlay-sabre.dts")
+    if("${KernelARMPlatform}" STREQUAL "")
+        message(STATUS "Selected platform imx6 supports multiple sub platforms but none were given")
+        message(STATUS "  Defaulting to sabre")
+        set(KernelARMPlatform sabre)
     endif()
-
+    list(FIND plat_lists ${KernelARMPlatform} index)
+    if("${index}" STREQUAL "-1")
+        message(FATAL_ERROR "Which imx6 platform not specified")
+    endif()
+    list(GET c_configs ${index} c_config)
+    list(GET cmake_configs ${index} cmake_config)
+    config_set(KernelARMPlatform ARM_PLAT ${KernelARMPlatform})
+    config_set(${cmake_config} ${c_config} ON)
+    list(APPEND KernelDTSList "tools/dts/${KernelARMPlatform}.dts")
+    list(APPEND KernelDTSList "src/plat/imx6/overlay-${KernelARMPlatform}.dts")
     declare_default_headers(
         TIMER_FREQUENCY 400000000llu
         MAX_IRQ 159
         INTERRUPT_CONTROLLER arch/machine/gic_pl390.h
         TIMER drivers/timer/arm_priv.h
     )
-else()
-    config_set(KernelPlatImx6 PLAT_IMX6 OFF)
 endif()
 
 add_sources(
diff --git a/src/plat/imx7/config.cmake b/src/plat/imx7/config.cmake
index c60cb59fd9eea03bbd801ad4d11e8f3f55adad90..e11c0477d725423650810056543746c5aa06f69e 100644
--- a/src/plat/imx7/config.cmake
+++ b/src/plat/imx7/config.cmake
@@ -12,11 +12,13 @@
 
 cmake_minimum_required(VERSION 3.7.2)
 
-if(KernelPlatformImx7Sabre)
+declare_platform(imx7 KernelPlatImx7 PLAT_IMX7_SABRE KernelSel4ArchAarch32)
+
+if(KernelPlatImx7)
+    declare_seL4_arch(aarch32)
     set(KernelArmCortexA7 ON)
     set(KernelArchArmV7a ON)
-    config_set(KernelPlatImx7 PLAT_IMX7 ON)
-    config_set(KernelPlatform PLAT "imx7")
+    config_set(KernelARMPlatform ARM_PLAT imx7sabre)
     set(KernelArmMach "imx" CACHE INTERNAL "")
     list(APPEND KernelDTSList "tools/dts/imx7sabre.dts")
     list(APPEND KernelDTSList "src/plat/imx7/overlay-imx7sabre.dts")
diff --git a/src/plat/odroidc2/config.cmake b/src/plat/odroidc2/config.cmake
index f19cb3a911f3c6b32b5887c42cc9f681b5216274..a009515e17e6f41bbbe76cb5793d62f4cf0fdc86 100644
--- a/src/plat/odroidc2/config.cmake
+++ b/src/plat/odroidc2/config.cmake
@@ -12,10 +12,13 @@
 
 cmake_minimum_required(VERSION 3.7.2)
 
+declare_platform(odroidc2 KernelPlatformOdroidc2 PLAT_ODROIDC2 KernelSel4ArchAarch64)
+
 if(KernelPlatformOdroidc2)
+    declare_seL4_arch(aarch64)
     set(KernelArmCortexA53 ON)
     set(KernelArchArmV8a ON)
-    config_set(KernelPlatform PLAT "odroidc2")
+    config_set(KernelARMPlatform ARM_PLAT odroidc2)
     set(KernelArmMachFeatureModifiers "+crc" CACHE INTERNAL "")
     list(APPEND KernelDTSList "tools/dts/odroidc2.dts")
     declare_default_headers(
diff --git a/src/plat/omap3/config.cmake b/src/plat/omap3/config.cmake
index 05d4431335ad572c79000cdac5440199dffcdd0d..f5d3ad87e4e858a0a5cde88cd682e3c67aea585a 100644
--- a/src/plat/omap3/config.cmake
+++ b/src/plat/omap3/config.cmake
@@ -12,10 +12,13 @@
 
 cmake_minimum_required(VERSION 3.7.2)
 
+declare_platform(omap3 KernelPlatformOMAP3 PLAT_OMAP3 KernelSel4ArchAarch32)
+
 if(KernelPlatformOMAP3)
+    declare_seL4_arch(aarch32)
     set(KernelArmCortexA8 ON)
     set(KernelArchArmV7a ON)
-    config_set(KernelPlatform PLAT "omap3")
+    config_set(KernelARMPlatform ARM_PLAT omap3)
     config_set(KernelArmMach MACH "omap")
     list(APPEND KernelDTSList "tools/dts/omap3.dts")
     list(APPEND KernelDTSList "src/plat/omap3/overlay-omap3.dts")
diff --git a/src/plat/pc99/config.cmake b/src/plat/pc99/config.cmake
index b3dc63ddd66e124880e68aacf08ce46336722ce9..2fac9de60164900b2bc9e90036c3ac9e71c3794d 100644
--- a/src/plat/pc99/config.cmake
+++ b/src/plat/pc99/config.cmake
@@ -12,6 +12,21 @@
 
 cmake_minimum_required(VERSION 3.7.2)
 
+declare_platform(pc99 KernelPlatPC99 PLAT_PC99 KernelArchX86)
+
+if(KernelPlatPC99)
+    if("${KernelSel4Arch}" STREQUAL ia32)
+        declare_seL4_arch(ia32)
+    elseif("${KernelSel4Arch}" STREQUAL x86_64)
+        declare_seL4_arch(x86_64)
+    else()
+        message(STATUS "Selected platform pc99 supports multiple architectures but none were given")
+        message(STATUS "  Defaulting to x86_64")
+        declare_seL4_arch(x86_64)
+    endif()
+
+endif()
+
 config_option(
     KernelIOMMU IOMMU "IOMMU support for VT-d enabled chipset"
     DEFAULT ON
diff --git a/src/plat/spike/config.cmake b/src/plat/spike/config.cmake
index 8d44c5cf06047ca5e3334b9b11efed5ba187d8a7..bedf95a692aeb2dafda138966dd46c6231a732d4 100644
--- a/src/plat/spike/config.cmake
+++ b/src/plat/spike/config.cmake
@@ -14,8 +14,21 @@
 
 cmake_minimum_required(VERSION 3.7.2)
 
+declare_platform(spike KernelPlatformSpike PLAT_SPIKE KernelArchRiscV)
+
 if(KernelPlatformSpike)
-    config_set(KernelPlatform PLAT "spike")
+    if("${KernelSel4Arch}" STREQUAL riscv32)
+        declare_seL4_arch(riscv32)
+    elseif("${KernelSel4Arch}" STREQUAL riscv64)
+        declare_seL4_arch(riscv64)
+    else()
+        message(
+            STATUS "Selected platform spike supports multiple architectures but none were given"
+        )
+        message(STATUS "  Defaulting to riscv64")
+        declare_seL4_arch(riscv64)
+    endif()
+    config_set(KernelRiscVPlatform RISCV_PLAT "spike")
     config_set(KernelPlatformFirstHartID FIRST_HART_ID 0)
     if(KernelSel4ArchRiscV32)
         list(APPEND KernelDTSList "tools/dts/spike32.dts")
@@ -26,4 +39,6 @@ if(KernelPlatformSpike)
         TIMER_FREQUENCY 10000000llu PLIC_MAX_NUM_INT 0
         INTERRUPT_CONTROLLER arch/machine/plic.h
     )
+else()
+    unset(KernelPlatformFirstHartID CACHE)
 endif()
diff --git a/src/plat/tk1/config.cmake b/src/plat/tk1/config.cmake
index d6a91919577365f6ec97edb4fcd4b06588852854..862f9be1e7998d0758511a9cce3f2c1a4f37eda1 100644
--- a/src/plat/tk1/config.cmake
+++ b/src/plat/tk1/config.cmake
@@ -12,11 +12,22 @@
 
 cmake_minimum_required(VERSION 3.7.2)
 
+declare_platform(tk1 KernelPlatformTK1 PLAT_TK1 "KernelSel4ArchAarch32 OR KernelSel4ArchArmHyp")
+
 if(KernelPlatformTK1)
+    if("${KernelSel4Arch}" STREQUAL aarch32)
+        declare_seL4_arch(aarch32)
+    elseif("${KernelSel4Arch}" STREQUAL arm_hyp)
+        declare_seL4_arch(arm_hyp)
+    else()
+        message(STATUS "Selected platform tk1 supports multiple architectures but none were given")
+        message(STATUS "  Defaulting to aarch32")
+        declare_seL4_arch(aarch32)
+    endif()
     set(KernelArmCortexA15 ON)
     set(KernelArchArmV7a ON)
     set(KernelArchArmV7ve ON)
-    config_set(KernelPlatform PLAT "tk1")
+    config_set(KernelARMPlatform ARM_PLAT tk1)
     config_set(KernelArmMach MACH "nvidia")
     list(APPEND KernelDTSList "tools/dts/tk1.dts")
     list(APPEND KernelDTSList "src/plat/tk1/overlay-tk1.dts")
diff --git a/src/plat/tx1/config.cmake b/src/plat/tx1/config.cmake
index 677c358838d88316b3f5da5eb219bc9632dafd71..b4380bd36246ec0a9dba84cad50a187d8f02cd21 100644
--- a/src/plat/tx1/config.cmake
+++ b/src/plat/tx1/config.cmake
@@ -12,10 +12,13 @@
 
 cmake_minimum_required(VERSION 3.7.2)
 
+declare_platform(tx1 KernelPlatformTx1 PLAT_TX1 KernelSel4ArchAarch64)
+
 if(KernelPlatformTx1)
+    declare_seL4_arch(aarch64)
     set(KernelArmCortexA57 ON)
     set(KernelArchArmV8a ON)
-    config_set(KernelPlatform PLAT "tx1")
+    config_set(KernelARMPlatform ARM_PLAT tx1)
     config_set(KernelArmMach MACH "nvidia")
     set(KernelArmPASizeBits44 ON)
     list(APPEND KernelDTSList "tools/dts/tx1.dts")
diff --git a/src/plat/tx2/config.cmake b/src/plat/tx2/config.cmake
index 3a339be7f2236fd578edd05708d1ebe0b4316557..618cfdb050dc4d4f288a6107f02a6b2873aaee65 100644
--- a/src/plat/tx2/config.cmake
+++ b/src/plat/tx2/config.cmake
@@ -12,10 +12,13 @@
 
 cmake_minimum_required(VERSION 3.7.2)
 
+declare_platform(tx2 KernelPlatformTx2 PLAT_TX2 KernelSel4ArchAarch64)
+
 if(KernelPlatformTx2)
+    declare_seL4_arch(aarch64)
     set(KernelArmCortexA57 ON)
     set(KernelArchArmV8a ON)
-    config_set(KernelPlatform PLAT "tx2")
+    config_set(KernelARMPlatform ARM_PLAT tx2)
     config_set(KernelArmMach MACH "nvidia")
     # Note that the 44-bit PA is only for Cortex-A57 cores.
     # If we enable the Denver 2 cores, which support 40-bit PA,
diff --git a/src/plat/zynq7000/config.cmake b/src/plat/zynq7000/config.cmake
index 7560d3b388fc28fc57714e94971b533fe3017d44..ce65c2185525c6204f24c8c31a545b03af1471db 100644
--- a/src/plat/zynq7000/config.cmake
+++ b/src/plat/zynq7000/config.cmake
@@ -12,10 +12,13 @@
 
 cmake_minimum_required(VERSION 3.7.2)
 
+declare_platform(zynq7000 KernelPlatformZynq7000 PLAT_ZYNQ7000 KernelSel4ArchAarch32)
+
 if(KernelPlatformZynq7000)
+    declare_seL4_arch(aarch32)
     set(KernelArmCortexA9 ON)
     set(KernelArchArmV7a ON)
-    config_set(KernelPlatform PLAT "zynq7000")
+    config_set(KernelARMPlatform ARM_PLAT zynq7000)
     config_set(KernelArmMach MACH "zynq")
     list(APPEND KernelDTSList "tools/dts/zynq7000.dts")
     declare_default_headers(
diff --git a/src/plat/zynqmp/config.cmake b/src/plat/zynqmp/config.cmake
index bb71f16f4197ba008124e5e48713e437949a8cf4..c17799ea1d3ccaad840d2a8a3d9aebf95e50f8df 100644
--- a/src/plat/zynqmp/config.cmake
+++ b/src/plat/zynqmp/config.cmake
@@ -12,17 +12,30 @@
 
 cmake_minimum_required(VERSION 3.7.2)
 
+declare_platform(ultra96 KernelPlatformUltra96 PLAT_ZYNQMP_ULTRA96 KernelArchARM)
+declare_platform(zynqmp KernelPlatformZynqmp PLAT_ZYNQMP KernelArchARM)
+
 if(KernelPlatformUltra96)
     # Ultra96 is is basically Zynqmp
     list(APPEND KernelDTSList "tools/dts/ultra96.dts")
     config_set(KernelPlatformZynqmp PLAT_ZYNQMP ON)
-    config_set(KernelPlatformZynqmpUltra96 PLAT_ZYNQMP_ULTRA96 ON)
 endif()
 
 if(KernelPlatformZynqmp)
+    if("${KernelSel4Arch}" STREQUAL aarch32)
+        declare_seL4_arch(aarch32)
+    elseif("${KernelSel4Arch}" STREQUAL aarch64)
+        declare_seL4_arch(aarch64)
+    else()
+        message(
+            STATUS "Selected platform zynqmp supports multiple architectures but none were given"
+        )
+        message(STATUS "  Defaulting to aarch64")
+        declare_seL4_arch(aarch64)
+    endif()
     set(KernelArmCortexA53 ON)
     set(KernelArchArmV8a ON)
-    config_set(KernelPlatform PLAT "zynqmp")
+    config_set(KernelARMPlatform ARM_PLAT zynqmp)
     config_set(KernelArmMach MACH "zynq")
 
     if(NOT KernelPlatformUltra96)