From c5b23791ea9f65efc4312c161dd173b7238c5e80 Mon Sep 17 00:00:00 2001
From: Gerwin Klein <gerwin.klein@proofcraft.systems>
Date: Sat, 28 Sep 2024 09:20:54 +0200
Subject: [PATCH] configs: additional verified platforms

With recent proof improvements the proofs now apply to further platforms
in the ARM and AARCH64 configurations.

Refactor the verified configs to build on one include file per major
architecture which is then used for each platform with potentially
modified settings. Add path argument to `cmake_script_build_kernel`
macro to accommodate inclusion from different locations in the file
system.

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
---
 configs/AARCH64_bcm2711_verified.cmake        | 20 ++------------
 configs/AARCH64_hikey_verified.cmake          | 10 +++++++
 configs/AARCH64_odroidc2_verified.cmake       | 10 +++++++
 configs/AARCH64_odroidc4_verified.cmake       | 10 +++++++
 configs/AARCH64_verified.cmake                | 23 ++--------------
 configs/AARCH64_zynqmp_verified.cmake         | 20 ++------------
 configs/ARM_HYP_exynos5410_verified.cmake     | 11 ++++++++
 configs/ARM_HYP_exynos5_verified.cmake        | 20 ++------------
 configs/ARM_HYP_verified.cmake                | 20 ++------------
 configs/ARM_MCS_verified.cmake                | 20 ++------------
 configs/ARM_exynos4_verified.cmake            | 10 +++++++
 configs/ARM_exynos5410_verified.cmake         | 11 ++++++++
 configs/ARM_exynos5422_verified.cmake         | 11 ++++++++
 configs/ARM_hikey_verified.cmake              | 10 +++++++
 configs/ARM_imx8mm_verified.cmake             | 21 +++------------
 configs/ARM_tk1_verified.cmake                | 10 +++++++
 configs/ARM_verified.cmake                    | 19 ++-----------
 configs/ARM_zynq7000_verified.cmake           | 10 +++++++
 configs/ARM_zynqmp_verified.cmake             | 10 +++++++
 configs/RISCV64_MCS_verified.cmake            | 21 +--------------
 configs/RISCV64_verified.cmake                | 23 ++--------------
 configs/X64_verified.cmake                    |  4 +--
 .../include/AARCH64_verified_include.cmake    | 24 +++++++++++++++++
 .../include/ARM_HYP_verified_include.cmake    |  9 +++++++
 configs/include/ARM_verified_include.cmake    | 24 +++++++++++++++++
 .../include/RISCV64_verified_include.cmake    | 27 +++++++++++++++++++
 tools/helpers.cmake                           |  4 +--
 27 files changed, 221 insertions(+), 191 deletions(-)
 create mode 100755 configs/AARCH64_hikey_verified.cmake
 create mode 100755 configs/AARCH64_odroidc2_verified.cmake
 create mode 100755 configs/AARCH64_odroidc4_verified.cmake
 create mode 100755 configs/ARM_HYP_exynos5410_verified.cmake
 create mode 100755 configs/ARM_exynos4_verified.cmake
 create mode 100755 configs/ARM_exynos5410_verified.cmake
 create mode 100755 configs/ARM_exynos5422_verified.cmake
 create mode 100755 configs/ARM_hikey_verified.cmake
 create mode 100755 configs/ARM_tk1_verified.cmake
 create mode 100755 configs/ARM_zynq7000_verified.cmake
 create mode 100755 configs/ARM_zynqmp_verified.cmake
 create mode 100644 configs/include/AARCH64_verified_include.cmake
 create mode 100644 configs/include/ARM_HYP_verified_include.cmake
 create mode 100644 configs/include/ARM_verified_include.cmake
 create mode 100644 configs/include/RISCV64_verified_include.cmake

diff --git a/configs/AARCH64_bcm2711_verified.cmake b/configs/AARCH64_bcm2711_verified.cmake
index 1bbb1552a..2060fb0e0 100755
--- a/configs/AARCH64_bcm2711_verified.cmake
+++ b/configs/AARCH64_bcm2711_verified.cmake
@@ -1,26 +1,10 @@
 #!/usr/bin/env -S cmake -P
 #
-# Copyright 2022, Proofcraft Pty Ltd
-# Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
+# Copyright 2024, Proofcraft Pty Ltd
 #
 # SPDX-License-Identifier: GPL-2.0-only
 #
 
-# If this file is executed then build the kernel.elf and kernel_all_pp.c file
-include(${CMAKE_CURRENT_LIST_DIR}/../tools/helpers.cmake)
-cmake_script_build_kernel()
+include(${CMAKE_CURRENT_LIST_DIR}/include/AARCH64_verified_include.cmake)
 
 set(KernelPlatform "bcm2711" CACHE STRING "")
-set(KernelSel4Arch "aarch64" CACHE STRING "")
-set(KernelArmHypervisorSupport ON CACHE BOOL "")
-set(KernelVerificationBuild ON CACHE BOOL "")
-set(KernelMaxNumNodes "1" CACHE STRING "")
-set(KernelOptimisation "-O2" CACHE STRING "")
-set(KernelRetypeFanOutLimit "256" CACHE STRING "")
-set(KernelBenchmarks "none" CACHE STRING "")
-set(KernelDangerousCodeInjection OFF CACHE BOOL "")
-set(KernelFastpath ON CACHE BOOL "")
-set(KernelPrinting OFF CACHE BOOL "")
-set(KernelNumDomains 16 CACHE STRING "")
-set(KernelMaxNumBootinfoUntypedCaps 50 CACHE STRING "")
-set(KernelArmSMMU OFF CACHE BOOL "")
diff --git a/configs/AARCH64_hikey_verified.cmake b/configs/AARCH64_hikey_verified.cmake
new file mode 100755
index 000000000..4609b1dec
--- /dev/null
+++ b/configs/AARCH64_hikey_verified.cmake
@@ -0,0 +1,10 @@
+#!/usr/bin/env -S cmake -P
+#
+# Copyright 2024, Proofcraft Pty Ltd
+#
+# SPDX-License-Identifier: GPL-2.0-only
+#
+
+include(${CMAKE_CURRENT_LIST_DIR}/include/AARCH64_verified_include.cmake)
+
+set(KernelPlatform "hikey" CACHE STRING "")
diff --git a/configs/AARCH64_odroidc2_verified.cmake b/configs/AARCH64_odroidc2_verified.cmake
new file mode 100755
index 000000000..7d6c74ed5
--- /dev/null
+++ b/configs/AARCH64_odroidc2_verified.cmake
@@ -0,0 +1,10 @@
+#!/usr/bin/env -S cmake -P
+#
+# Copyright 2024, Proofcraft Pty Ltd
+#
+# SPDX-License-Identifier: GPL-2.0-only
+#
+
+include(${CMAKE_CURRENT_LIST_DIR}/include/AARCH64_verified_include.cmake)
+
+set(KernelPlatform "odroidc2" CACHE STRING "")
diff --git a/configs/AARCH64_odroidc4_verified.cmake b/configs/AARCH64_odroidc4_verified.cmake
new file mode 100755
index 000000000..430052539
--- /dev/null
+++ b/configs/AARCH64_odroidc4_verified.cmake
@@ -0,0 +1,10 @@
+#!/usr/bin/env -S cmake -P
+#
+# Copyright 2024, Proofcraft Pty Ltd
+#
+# SPDX-License-Identifier: GPL-2.0-only
+#
+
+include(${CMAKE_CURRENT_LIST_DIR}/include/AARCH64_verified_include.cmake)
+
+set(KernelPlatform "odroidc4" CACHE STRING "")
diff --git a/configs/AARCH64_verified.cmake b/configs/AARCH64_verified.cmake
index 263de52fa..e0c28df57 100755
--- a/configs/AARCH64_verified.cmake
+++ b/configs/AARCH64_verified.cmake
@@ -1,29 +1,10 @@
 #!/usr/bin/env -S cmake -P
 #
-# Copyright 2022, Proofcraft Pty Ltd
-# Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
+# Copyright 2024, Proofcraft Pty Ltd
 #
 # SPDX-License-Identifier: GPL-2.0-only
 #
 
-# This is a preliminary configuration to be used for developing functional
-# correctness proofs for the AArch64 architecture.
-
-# If this file is executed then build the kernel.elf and kernel_all_pp.c file
-include(${CMAKE_CURRENT_LIST_DIR}/../tools/helpers.cmake)
-cmake_script_build_kernel()
+include(${CMAKE_CURRENT_LIST_DIR}/include/AARCH64_verified_include.cmake)
 
 set(KernelPlatform "tx2" CACHE STRING "")
-set(KernelSel4Arch "aarch64" CACHE STRING "")
-set(KernelArmHypervisorSupport ON CACHE BOOL "")
-set(KernelVerificationBuild ON CACHE BOOL "")
-set(KernelMaxNumNodes "1" CACHE STRING "")
-set(KernelOptimisation "-O2" CACHE STRING "")
-set(KernelRetypeFanOutLimit "256" CACHE STRING "")
-set(KernelBenchmarks "none" CACHE STRING "")
-set(KernelDangerousCodeInjection OFF CACHE BOOL "")
-set(KernelFastpath ON CACHE BOOL "")
-set(KernelPrinting OFF CACHE BOOL "")
-set(KernelNumDomains 16 CACHE STRING "")
-set(KernelMaxNumBootinfoUntypedCaps 50 CACHE STRING "")
-set(KernelArmSMMU OFF CACHE BOOL "")
diff --git a/configs/AARCH64_zynqmp_verified.cmake b/configs/AARCH64_zynqmp_verified.cmake
index aa16396d4..564964b21 100755
--- a/configs/AARCH64_zynqmp_verified.cmake
+++ b/configs/AARCH64_zynqmp_verified.cmake
@@ -1,26 +1,10 @@
 #!/usr/bin/env -S cmake -P
 #
-# Copyright 2022, Proofcraft Pty Ltd
-# Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
+# Copyright 2024, Proofcraft Pty Ltd
 #
 # SPDX-License-Identifier: GPL-2.0-only
 #
 
-# If this file is executed then build the kernel.elf and kernel_all_pp.c file
-include(${CMAKE_CURRENT_LIST_DIR}/../tools/helpers.cmake)
-cmake_script_build_kernel()
+include(${CMAKE_CURRENT_LIST_DIR}/include/AARCH64_verified_include.cmake)
 
 set(KernelPlatform "zynqmp" CACHE STRING "")
-set(KernelSel4Arch "aarch64" CACHE STRING "")
-set(KernelArmHypervisorSupport ON CACHE BOOL "")
-set(KernelVerificationBuild ON CACHE BOOL "")
-set(KernelMaxNumNodes "1" CACHE STRING "")
-set(KernelOptimisation "-O2" CACHE STRING "")
-set(KernelRetypeFanOutLimit "256" CACHE STRING "")
-set(KernelBenchmarks "none" CACHE STRING "")
-set(KernelDangerousCodeInjection OFF CACHE BOOL "")
-set(KernelFastpath ON CACHE BOOL "")
-set(KernelPrinting OFF CACHE BOOL "")
-set(KernelNumDomains 16 CACHE STRING "")
-set(KernelMaxNumBootinfoUntypedCaps 50 CACHE STRING "")
-set(KernelArmSMMU OFF CACHE BOOL "")
diff --git a/configs/ARM_HYP_exynos5410_verified.cmake b/configs/ARM_HYP_exynos5410_verified.cmake
new file mode 100755
index 000000000..665115ecc
--- /dev/null
+++ b/configs/ARM_HYP_exynos5410_verified.cmake
@@ -0,0 +1,11 @@
+#!/usr/bin/env -S cmake -P
+#
+# Copyright 2024, Proofcraft Pty Ltd
+#
+# SPDX-License-Identifier: GPL-2.0-only
+#
+
+include(${CMAKE_CURRENT_LIST_DIR}/include/ARM_HYP_verified_include.cmake)
+
+set(KernelPlatform "exynos5" CACHE STRING "")
+set(KernelARMPlatform "exynos5410" CACHE STRING "")
diff --git a/configs/ARM_HYP_exynos5_verified.cmake b/configs/ARM_HYP_exynos5_verified.cmake
index 398c31968..09a2016d9 100755
--- a/configs/ARM_HYP_exynos5_verified.cmake
+++ b/configs/ARM_HYP_exynos5_verified.cmake
@@ -1,27 +1,11 @@
 #!/usr/bin/env -S cmake -P
 #
-# Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
+# Copyright 2024, Proofcraft Pty Ltd
 #
 # SPDX-License-Identifier: GPL-2.0-only
 #
 
-# If this file is executed then build the kernel.elf and kernel_all_pp.c file
-include(${CMAKE_CURRENT_LIST_DIR}/../tools/helpers.cmake)
-cmake_script_build_kernel()
+include(${CMAKE_CURRENT_LIST_DIR}/include/ARM_HYP_verified_include.cmake)
 
 set(KernelPlatform "exynos5" CACHE STRING "")
 set(KernelARMPlatform "exynos5422" CACHE STRING "")
-set(KernelSel4Arch "arm_hyp" CACHE STRING "")
-set(KernelAArch32FPUEnableContextSwitch OFF CACHE BOOL "")
-set(KernelVerificationBuild ON CACHE BOOL "")
-set(KernelIPCBufferLocation "threadID_register" CACHE STRING "")
-set(KernelMaxNumNodes "1" CACHE STRING "")
-set(KernelOptimisation "-O2" CACHE STRING "")
-set(KernelRetypeFanOutLimit "256" CACHE STRING "")
-set(KernelBenchmarks "none" CACHE STRING "")
-set(KernelDangerousCodeInjection OFF CACHE BOOL "")
-set(KernelFastpath ON CACHE BOOL "")
-set(KernelPrinting OFF CACHE BOOL "")
-set(KernelNumDomains 16 CACHE STRING "")
-set(KernelRootCNodeSizeBits 19 CACHE STRING "")
-set(KernelMaxNumBootinfoUntypedCaps 50 CACHE STRING "")
diff --git a/configs/ARM_HYP_verified.cmake b/configs/ARM_HYP_verified.cmake
index d698a2bae..e62d53917 100755
--- a/configs/ARM_HYP_verified.cmake
+++ b/configs/ARM_HYP_verified.cmake
@@ -1,26 +1,10 @@
 #!/usr/bin/env -S cmake -P
 #
-# Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
+# Copyright 2024, Proofcraft Pty Ltd
 #
 # SPDX-License-Identifier: GPL-2.0-only
 #
 
-# If this file is executed then build the kernel.elf and kernel_all_pp.c file
-include(${CMAKE_CURRENT_LIST_DIR}/../tools/helpers.cmake)
-cmake_script_build_kernel()
+include(${CMAKE_CURRENT_LIST_DIR}/include/ARM_HYP_verified_include.cmake)
 
 set(KernelPlatform "tk1" CACHE STRING "")
-set(KernelSel4Arch "arm_hyp" CACHE STRING "")
-set(KernelAArch32FPUEnableContextSwitch OFF CACHE BOOL "")
-set(KernelVerificationBuild ON CACHE BOOL "")
-set(KernelIPCBufferLocation "threadID_register" CACHE STRING "")
-set(KernelMaxNumNodes "1" CACHE STRING "")
-set(KernelOptimisation "-O2" CACHE STRING "")
-set(KernelRetypeFanOutLimit "256" CACHE STRING "")
-set(KernelBenchmarks "none" CACHE STRING "")
-set(KernelDangerousCodeInjection OFF CACHE BOOL "")
-set(KernelFastpath ON CACHE BOOL "")
-set(KernelPrinting OFF CACHE BOOL "")
-set(KernelNumDomains 16 CACHE STRING "")
-set(KernelRootCNodeSizeBits 19 CACHE STRING "")
-set(KernelMaxNumBootinfoUntypedCaps 50 CACHE STRING "")
diff --git a/configs/ARM_MCS_verified.cmake b/configs/ARM_MCS_verified.cmake
index 5145c4ee9..96df4e6ba 100755
--- a/configs/ARM_MCS_verified.cmake
+++ b/configs/ARM_MCS_verified.cmake
@@ -1,28 +1,12 @@
 #!/usr/bin/env -S cmake -P
 #
-# Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
+# Copyright 2024, Proofcraft Pty Ltd
 #
 # SPDX-License-Identifier: GPL-2.0-only
 #
 
-# If this file is executed then build the kernel.elf and kernel_all_pp.c file
-include(${CMAKE_CURRENT_LIST_DIR}/../tools/helpers.cmake)
-cmake_script_build_kernel()
+include(${CMAKE_CURRENT_LIST_DIR}/include/ARM_verified_include.cmake)
 
 set(KernelPlatform "imx6" CACHE STRING "")
-set(KernelAArch32FPUEnableContextSwitch OFF CACHE BOOL "")
-set(KernelVerificationBuild ON CACHE BOOL "")
-set(KernelBinaryVerificationBuild ON CACHE BOOL "")
-set(KernelOptimisationCloneFunctions OFF CACHE BOOL "")
-set(KernelIPCBufferLocation "threadID_register" CACHE STRING "")
-set(KernelMaxNumNodes "1" CACHE STRING "")
-set(KernelOptimisation "-O2" CACHE STRING "")
-set(KernelRetypeFanOutLimit "256" CACHE STRING "")
-set(KernelBenchmarks "none" CACHE STRING "")
-set(KernelDangerousCodeInjection OFF CACHE BOOL "")
-set(KernelFastpath ON CACHE BOOL "")
-set(KernelPrinting OFF CACHE BOOL "")
-set(KernelNumDomains 16 CACHE STRING "")
-set(KernelMaxNumBootinfoUntypedCaps 230 CACHE STRING "")
 set(KernelIsMCS ON CACHE BOOL "")
 set(KernelStaticMaxPeriodUs "(60 * 60 * MS_IN_S * US_IN_MS)" CACHE STRING "")
diff --git a/configs/ARM_exynos4_verified.cmake b/configs/ARM_exynos4_verified.cmake
new file mode 100755
index 000000000..7c1f858b5
--- /dev/null
+++ b/configs/ARM_exynos4_verified.cmake
@@ -0,0 +1,10 @@
+#!/usr/bin/env -S cmake -P
+#
+# Copyright 2024, Proofcraft Pty Ltd
+#
+# SPDX-License-Identifier: GPL-2.0-only
+#
+
+include(${CMAKE_CURRENT_LIST_DIR}/include/ARM_verified_include.cmake)
+
+set(KernelPlatform "exynos4" CACHE STRING "")
diff --git a/configs/ARM_exynos5410_verified.cmake b/configs/ARM_exynos5410_verified.cmake
new file mode 100755
index 000000000..ea309ef5e
--- /dev/null
+++ b/configs/ARM_exynos5410_verified.cmake
@@ -0,0 +1,11 @@
+#!/usr/bin/env -S cmake -P
+#
+# Copyright 2024, Proofcraft Pty Ltd
+#
+# SPDX-License-Identifier: GPL-2.0-only
+#
+
+include(${CMAKE_CURRENT_LIST_DIR}/include/ARM_verified_include.cmake)
+
+set(KernelPlatform "exynos5" CACHE STRING "")
+set(KernelARMPlatform "exynos5410" CACHE STRING "")
diff --git a/configs/ARM_exynos5422_verified.cmake b/configs/ARM_exynos5422_verified.cmake
new file mode 100755
index 000000000..5e7daa4ea
--- /dev/null
+++ b/configs/ARM_exynos5422_verified.cmake
@@ -0,0 +1,11 @@
+#!/usr/bin/env -S cmake -P
+#
+# Copyright 2024, Proofcraft Pty Ltd
+#
+# SPDX-License-Identifier: GPL-2.0-only
+#
+
+include(${CMAKE_CURRENT_LIST_DIR}/include/ARM_verified_include.cmake)
+
+set(KernelPlatform "exynos5" CACHE STRING "")
+set(KernelARMPlatform "exynos5422" CACHE STRING "")
diff --git a/configs/ARM_hikey_verified.cmake b/configs/ARM_hikey_verified.cmake
new file mode 100755
index 000000000..9607dcf32
--- /dev/null
+++ b/configs/ARM_hikey_verified.cmake
@@ -0,0 +1,10 @@
+#!/usr/bin/env -S cmake -P
+#
+# Copyright 2024, Proofcraft Pty Ltd
+#
+# SPDX-License-Identifier: GPL-2.0-only
+#
+
+include(${CMAKE_CURRENT_LIST_DIR}/include/ARM_verified_include.cmake)
+
+set(KernelPlatform "hikey" CACHE STRING "")
diff --git a/configs/ARM_imx8mm_verified.cmake b/configs/ARM_imx8mm_verified.cmake
index 53050d6c8..46ad543da 100755
--- a/configs/ARM_imx8mm_verified.cmake
+++ b/configs/ARM_imx8mm_verified.cmake
@@ -1,26 +1,11 @@
 #!/usr/bin/env -S cmake -P
 #
-# Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
+# Copyright 2024, Proofcraft Pty Ltd
 #
 # SPDX-License-Identifier: GPL-2.0-only
 #
 
-# If this file is executed then build the kernel.elf and kernel_all_pp.c file
-include(${CMAKE_CURRENT_LIST_DIR}/../tools/helpers.cmake)
-cmake_script_build_kernel()
+include(${CMAKE_CURRENT_LIST_DIR}/include/ARM_verified_include.cmake)
 
 set(KernelPlatform "imx8mm-evk" CACHE STRING "")
-set(KernelSel4Arch "aarch32" CACHE STRING "")
-set(KernelAArch32FPUEnableContextSwitch ON CACHE BOOL "")
-set(KernelVerificationBuild ON CACHE BOOL "")
-set(KernelBinaryVerificationBuild ON CACHE BOOL "")
-set(KernelOptimisationCloneFunctions OFF CACHE BOOL "")
-set(KernelIPCBufferLocation "threadID_register" CACHE STRING "")
-set(KernelMaxNumNodes "1" CACHE STRING "")
-set(KernelOptimisation "-O2" CACHE STRING "")
-set(KernelRetypeFanOutLimit "256" CACHE STRING "")
-set(KernelBenchmarks "none" CACHE STRING "")
-set(KernelDangerousCodeInjection OFF CACHE BOOL "")
-set(KernelFastpath ON CACHE BOOL "")
-set(KernelPrinting OFF CACHE BOOL "")
-set(KernelNumDomains 16 CACHE STRING "")
+set(KernelAArch32FPUEnableContextSwitch ON CACHE BOOL "" FORCE)
diff --git a/configs/ARM_tk1_verified.cmake b/configs/ARM_tk1_verified.cmake
new file mode 100755
index 000000000..62144de96
--- /dev/null
+++ b/configs/ARM_tk1_verified.cmake
@@ -0,0 +1,10 @@
+#!/usr/bin/env -S cmake -P
+#
+# Copyright 2024, Proofcraft Pty Ltd
+#
+# SPDX-License-Identifier: GPL-2.0-only
+#
+
+include(${CMAKE_CURRENT_LIST_DIR}/include/ARM_verified_include.cmake)
+
+set(KernelPlatform "tk1" CACHE STRING "")
diff --git a/configs/ARM_verified.cmake b/configs/ARM_verified.cmake
index 55c636762..555ec6568 100755
--- a/configs/ARM_verified.cmake
+++ b/configs/ARM_verified.cmake
@@ -1,25 +1,10 @@
 #!/usr/bin/env -S cmake -P
 #
-# Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
+# Copyright 2024, Proofcraft Pty Ltd
 #
 # SPDX-License-Identifier: GPL-2.0-only
 #
 
-# If this file is executed then build the kernel.elf and kernel_all_pp.c file
-include(${CMAKE_CURRENT_LIST_DIR}/../tools/helpers.cmake)
-cmake_script_build_kernel()
+include(${CMAKE_CURRENT_LIST_DIR}/include/ARM_verified_include.cmake)
 
 set(KernelPlatform "imx6" CACHE STRING "")
-set(KernelAArch32FPUEnableContextSwitch OFF CACHE BOOL "")
-set(KernelVerificationBuild ON CACHE BOOL "")
-set(KernelBinaryVerificationBuild ON CACHE BOOL "")
-set(KernelOptimisationCloneFunctions OFF CACHE BOOL "")
-set(KernelIPCBufferLocation "threadID_register" CACHE STRING "")
-set(KernelMaxNumNodes "1" CACHE STRING "")
-set(KernelOptimisation "-O2" CACHE STRING "")
-set(KernelRetypeFanOutLimit "256" CACHE STRING "")
-set(KernelBenchmarks "none" CACHE STRING "")
-set(KernelDangerousCodeInjection OFF CACHE BOOL "")
-set(KernelFastpath ON CACHE BOOL "")
-set(KernelPrinting OFF CACHE BOOL "")
-set(KernelNumDomains 16 CACHE STRING "")
diff --git a/configs/ARM_zynq7000_verified.cmake b/configs/ARM_zynq7000_verified.cmake
new file mode 100755
index 000000000..5197cbdac
--- /dev/null
+++ b/configs/ARM_zynq7000_verified.cmake
@@ -0,0 +1,10 @@
+#!/usr/bin/env -S cmake -P
+#
+# Copyright 2024, Proofcraft Pty Ltd
+#
+# SPDX-License-Identifier: GPL-2.0-only
+#
+
+include(${CMAKE_CURRENT_LIST_DIR}/include/ARM_verified_include.cmake)
+
+set(KernelPlatform "zynq7000" CACHE STRING "")
diff --git a/configs/ARM_zynqmp_verified.cmake b/configs/ARM_zynqmp_verified.cmake
new file mode 100755
index 000000000..1ae3f5998
--- /dev/null
+++ b/configs/ARM_zynqmp_verified.cmake
@@ -0,0 +1,10 @@
+#!/usr/bin/env -S cmake -P
+#
+# Copyright 2024, Proofcraft Pty Ltd
+#
+# SPDX-License-Identifier: GPL-2.0-only
+#
+
+include(${CMAKE_CURRENT_LIST_DIR}/include/ARM_verified_include.cmake)
+
+set(KernelPlatform "zynqmp" CACHE STRING "")
diff --git a/configs/RISCV64_MCS_verified.cmake b/configs/RISCV64_MCS_verified.cmake
index 656eb031a..492eae0a1 100755
--- a/configs/RISCV64_MCS_verified.cmake
+++ b/configs/RISCV64_MCS_verified.cmake
@@ -5,27 +5,8 @@
 # SPDX-License-Identifier: GPL-2.0-only
 #
 
-# If this file is executed then build the kernel.elf and kernel_all_pp.c file
-include(${CMAKE_CURRENT_LIST_DIR}/../tools/helpers.cmake)
-cmake_script_build_kernel()
+include(${CMAKE_CURRENT_LIST_DIR}/include/RISCV64_verified_include.cmake)
 
-set(KernelSel4Arch "riscv64" CACHE STRING "")
 set(KernelPlatform "hifive" CACHE STRING "")
-set(KernelPTLevels "3" CACHE STRING "")
-set(KernelVerificationBuild ON CACHE BOOL "")
-set(KernelBinaryVerificationBuild ON CACHE BOOL "")
-set(KernelOptimisationCloneFunctions OFF CACHE BOOL "")
-set(KernelMaxNumNodes "1" CACHE STRING "")
-set(KernelOptimisation "-O2" CACHE STRING "")
-set(KernelRetypeFanOutLimit "256" CACHE STRING "")
-set(KernelBenchmarks "none" CACHE STRING "")
-set(KernelDangerousCodeInjection OFF CACHE BOOL "")
-set(KernelFastpath ON CACHE BOOL "")
-set(KernelPrinting OFF CACHE BOOL "")
-set(KernelNumDomains 16 CACHE STRING "")
-set(KernelRootCNodeSizeBits 19 CACHE STRING "")
-set(KernelMaxNumBootinfoUntypedCaps 50 CACHE STRING "")
 set(KernelIsMCS ON CACHE BOOL "")
 set(KernelStaticMaxPeriodUs "(60 * 60 * MS_IN_S * US_IN_MS)" CACHE STRING "")
-set(KernelClzNoBuiltin ON CACHE BOOL "")
-set(KernelCtzNoBuiltin ON CACHE BOOL "")
diff --git a/configs/RISCV64_verified.cmake b/configs/RISCV64_verified.cmake
index d71b7612b..240a446d3 100755
--- a/configs/RISCV64_verified.cmake
+++ b/configs/RISCV64_verified.cmake
@@ -1,29 +1,10 @@
 #!/usr/bin/env -S cmake -P
 #
-# Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
+# Copyright 2024, Proofcraft Pty Ltd
 #
 # SPDX-License-Identifier: GPL-2.0-only
 #
 
-# If this file is executed then build the kernel.elf and kernel_all_pp.c file
-include(${CMAKE_CURRENT_LIST_DIR}/../tools/helpers.cmake)
-cmake_script_build_kernel()
+include(${CMAKE_CURRENT_LIST_DIR}/include/RISCV64_verified_include.cmake)
 
-set(KernelSel4Arch "riscv64" CACHE STRING "")
 set(KernelPlatform "hifive" CACHE STRING "")
-set(KernelPTLevels "3" CACHE STRING "")
-set(KernelVerificationBuild ON CACHE BOOL "")
-set(KernelBinaryVerificationBuild ON CACHE BOOL "")
-set(KernelOptimisationCloneFunctions OFF CACHE BOOL "")
-set(KernelMaxNumNodes "1" CACHE STRING "")
-set(KernelOptimisation "-O2" CACHE STRING "")
-set(KernelRetypeFanOutLimit "256" CACHE STRING "")
-set(KernelBenchmarks "none" CACHE STRING "")
-set(KernelDangerousCodeInjection OFF CACHE BOOL "")
-set(KernelFastpath ON CACHE BOOL "")
-set(KernelPrinting OFF CACHE BOOL "")
-set(KernelNumDomains 16 CACHE STRING "")
-set(KernelRootCNodeSizeBits 19 CACHE STRING "")
-set(KernelMaxNumBootinfoUntypedCaps 50 CACHE STRING "")
-set(KernelClzNoBuiltin ON CACHE BOOL "")
-set(KernelCtzNoBuiltin ON CACHE BOOL "")
diff --git a/configs/X64_verified.cmake b/configs/X64_verified.cmake
index b493f5366..33435fa89 100755
--- a/configs/X64_verified.cmake
+++ b/configs/X64_verified.cmake
@@ -5,9 +5,9 @@
 # SPDX-License-Identifier: GPL-2.0-only
 #
 
-# If this file is executed then build the kernel.elf and kernel_all_pp.c file
+# If this file is executed it will build the kernel.elf and kernel_all_pp.c file
 include(${CMAKE_CURRENT_LIST_DIR}/../tools/helpers.cmake)
-cmake_script_build_kernel()
+cmake_script_build_kernel(..)
 
 set(KernelPlatform "pc99" CACHE STRING "")
 set(KernelSel4Arch "x86_64" CACHE STRING "")
diff --git a/configs/include/AARCH64_verified_include.cmake b/configs/include/AARCH64_verified_include.cmake
new file mode 100644
index 000000000..e83c5fe09
--- /dev/null
+++ b/configs/include/AARCH64_verified_include.cmake
@@ -0,0 +1,24 @@
+#
+# Copyright 2022, Proofcraft Pty Ltd
+# Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
+#
+# SPDX-License-Identifier: GPL-2.0-only
+#
+
+# If this file is executed it will build the kernel.elf and kernel_all_pp.c file
+include(${CMAKE_CURRENT_LIST_DIR}/../../tools/helpers.cmake)
+cmake_script_build_kernel(../..)
+
+set(KernelSel4Arch "aarch64" CACHE STRING "")
+set(KernelArmHypervisorSupport ON CACHE BOOL "")
+set(KernelVerificationBuild ON CACHE BOOL "")
+set(KernelMaxNumNodes "1" CACHE STRING "")
+set(KernelOptimisation "-O2" CACHE STRING "")
+set(KernelRetypeFanOutLimit "256" CACHE STRING "")
+set(KernelBenchmarks "none" CACHE STRING "")
+set(KernelDangerousCodeInjection OFF CACHE BOOL "")
+set(KernelFastpath ON CACHE BOOL "")
+set(KernelPrinting OFF CACHE BOOL "")
+set(KernelNumDomains 16 CACHE STRING "")
+set(KernelMaxNumBootinfoUntypedCaps 50 CACHE STRING "")
+set(KernelArmSMMU OFF CACHE BOOL "")
diff --git a/configs/include/ARM_HYP_verified_include.cmake b/configs/include/ARM_HYP_verified_include.cmake
new file mode 100644
index 000000000..17862867c
--- /dev/null
+++ b/configs/include/ARM_HYP_verified_include.cmake
@@ -0,0 +1,9 @@
+#
+# Copyright 2024, Proofcraft Pty Ltd
+#
+# SPDX-License-Identifier: GPL-2.0-only
+#
+
+include(${CMAKE_CURRENT_LIST_DIR}/ARM_verified_include.cmake)
+
+set(KernelSel4Arch "arm_hyp" CACHE STRING "" FORCE)
diff --git a/configs/include/ARM_verified_include.cmake b/configs/include/ARM_verified_include.cmake
new file mode 100644
index 000000000..a9c62087d
--- /dev/null
+++ b/configs/include/ARM_verified_include.cmake
@@ -0,0 +1,24 @@
+#
+# Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
+#
+# SPDX-License-Identifier: GPL-2.0-only
+#
+
+# If this file is executed it will build the kernel.elf and kernel_all_pp.c file
+include(${CMAKE_CURRENT_LIST_DIR}/../../tools/helpers.cmake)
+cmake_script_build_kernel(../..)
+
+set(KernelSel4Arch "aarch32" CACHE STRING "")
+set(KernelAArch32FPUEnableContextSwitch OFF CACHE BOOL "")
+set(KernelVerificationBuild ON CACHE BOOL "")
+set(KernelBinaryVerificationBuild ON CACHE BOOL "")
+set(KernelOptimisationCloneFunctions OFF CACHE BOOL "")
+set(KernelIPCBufferLocation "threadID_register" CACHE STRING "")
+set(KernelMaxNumNodes "1" CACHE STRING "")
+set(KernelOptimisation "-O2" CACHE STRING "")
+set(KernelRetypeFanOutLimit "256" CACHE STRING "")
+set(KernelBenchmarks "none" CACHE STRING "")
+set(KernelDangerousCodeInjection OFF CACHE BOOL "")
+set(KernelFastpath ON CACHE BOOL "")
+set(KernelPrinting OFF CACHE BOOL "")
+set(KernelNumDomains 16 CACHE STRING "")
diff --git a/configs/include/RISCV64_verified_include.cmake b/configs/include/RISCV64_verified_include.cmake
new file mode 100644
index 000000000..4c7804618
--- /dev/null
+++ b/configs/include/RISCV64_verified_include.cmake
@@ -0,0 +1,27 @@
+#
+# Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
+#
+# SPDX-License-Identifier: GPL-2.0-only
+#
+
+# If this file is executed it will build the kernel.elf and kernel_all_pp.c file
+include(${CMAKE_CURRENT_LIST_DIR}/../../tools/helpers.cmake)
+cmake_script_build_kernel(../..)
+
+set(KernelSel4Arch "riscv64" CACHE STRING "")
+set(KernelPTLevels "3" CACHE STRING "")
+set(KernelVerificationBuild ON CACHE BOOL "")
+set(KernelBinaryVerificationBuild ON CACHE BOOL "")
+set(KernelOptimisationCloneFunctions OFF CACHE BOOL "")
+set(KernelMaxNumNodes "1" CACHE STRING "")
+set(KernelOptimisation "-O2" CACHE STRING "")
+set(KernelRetypeFanOutLimit "256" CACHE STRING "")
+set(KernelBenchmarks "none" CACHE STRING "")
+set(KernelDangerousCodeInjection OFF CACHE BOOL "")
+set(KernelFastpath ON CACHE BOOL "")
+set(KernelPrinting OFF CACHE BOOL "")
+set(KernelNumDomains 16 CACHE STRING "")
+set(KernelRootCNodeSizeBits 19 CACHE STRING "")
+set(KernelMaxNumBootinfoUntypedCaps 50 CACHE STRING "")
+set(KernelClzNoBuiltin ON CACHE BOOL "")
+set(KernelCtzNoBuiltin ON CACHE BOOL "")
diff --git a/tools/helpers.cmake b/tools/helpers.cmake
index f600e4693..312ad4898 100644
--- a/tools/helpers.cmake
+++ b/tools/helpers.cmake
@@ -688,7 +688,7 @@ endmacro()
 # cmake -G Ninja ${args} -C ${CMAKE_ARGV2} ${CMAKE_CURRENT_LIST_DIR}/..
 # ninja kernel.elf
 # ninja kernel_all_pp_wrapper
-macro(cmake_script_build_kernel)
+macro(cmake_script_build_kernel RELPATH)
     if(NOT "${CMAKE_ARGC}" STREQUAL "")
         set(args "")
         foreach(i RANGE 3 ${CMAKE_ARGC})
@@ -702,7 +702,7 @@ macro(cmake_script_build_kernel)
         endforeach()
         execute_process(
             COMMAND
-                cmake -G Ninja ${args} -C ${CMAKE_ARGV2} ${CMAKE_CURRENT_LIST_DIR}/..
+                cmake -G Ninja ${args} -C ${CMAKE_ARGV2} ${CMAKE_CURRENT_LIST_DIR}/${RELPATH}
             INPUT_FILE /dev/stdin
             OUTPUT_FILE /dev/stdout
             ERROR_FILE /dev/stderr