From b562dfbcfaaf94dbf828317b0c17e13e4c24afe3 Mon Sep 17 00:00:00 2001 From: Gerwin Klein Date: Sun, 23 Aug 2026 09:45:10 +0200 Subject: [PATCH 1/2] Add verified RISC-V platforms Add all RISC-V platforms to the verified list and update verified-configurations page accordingly now that RISC-V verification platform support has been merged. Signed-off-by: Gerwin Klein --- Hardware/Star64/index.md | 2 +- Hardware/ariane.md | 2 +- Hardware/bananapi-f3.md | 2 +- Hardware/cheshire.md | 2 +- Hardware/hifive-p550.md | 2 +- Hardware/polarfire.md | 2 +- Hardware/rocketchip-zcu102.md | 4 +-- Hardware/rocketchip.md | 2 +- Hardware/spike.md | 1 + projects/sel4/verified-configurations.md | 46 +++++++++++++----------- 10 files changed, 35 insertions(+), 30 deletions(-) diff --git a/Hardware/Star64/index.md b/Hardware/Star64/index.md index 786ecdc54fb..d1c239e651e 100644 --- a/Hardware/Star64/index.md +++ b/Hardware/Star64/index.md @@ -7,7 +7,7 @@ arch: RV64GBC, RV64IMAC, RV32IMAFBC virtualization: false iommu: false simulation_target: false -verification: [] +verification: [RISCV64] Contrib: "Community" Maintained: "seL4 Foundation" soc: StarFive JH7110 diff --git a/Hardware/ariane.md b/Hardware/ariane.md index 664cdfc1439..2ebc1b4f222 100644 --- a/Hardware/ariane.md +++ b/Hardware/ariane.md @@ -7,7 +7,7 @@ arch: RV64IMAC virtualization: false iommu: false simulation_target: false -verification: [] +verification: [RISCV64] Contrib: "Data61" Maintained: "Hensoldt Cyber" cpu: Ariane (CVA6) diff --git a/Hardware/bananapi-f3.md b/Hardware/bananapi-f3.md index dbc2717e23f..25648cc98ad 100644 --- a/Hardware/bananapi-f3.md +++ b/Hardware/bananapi-f3.md @@ -7,7 +7,7 @@ arch: RV64GCVB virtualization: false iommu: false simulation_target: false -verification: [] +verification: [RISCV64] Contrib: "Community" Maintained: "10xEngineers" soc: SpacemiT K1 diff --git a/Hardware/cheshire.md b/Hardware/cheshire.md index 6aeb52e5ac3..48a1c666ed9 100644 --- a/Hardware/cheshire.md +++ b/Hardware/cheshire.md @@ -7,7 +7,7 @@ arch: RV64IMAFDC virtualization: false iommu: false simulation_target: false -verification: [] +verification: [RISCV64] Contrib: "UNSW" Maintained: "UNSW" cpu: Cheshire diff --git a/Hardware/hifive-p550.md b/Hardware/hifive-p550.md index d34286803e7..e74e640ad9c 100644 --- a/Hardware/hifive-p550.md +++ b/Hardware/hifive-p550.md @@ -7,7 +7,7 @@ arch: RV64GC virtualization: false iommu: false simulation_target: false -verification: [] +verification: [RISCV64] Contrib: "Community" Maintained: "seL4 Foundation" soc: ESWIN EIC7700X diff --git a/Hardware/polarfire.md b/Hardware/polarfire.md index 96fa62dfcad..f2c74b08162 100644 --- a/Hardware/polarfire.md +++ b/Hardware/polarfire.md @@ -7,7 +7,7 @@ arch: RV64IMAC, RV64GC virtualization: false iommu: false simulation_target: false -verification: [] +verification: [RISCV64] Contrib: 'DornerWorks' Maintained: 'DornerWorks' soc: PolarFire SoC FPGA diff --git a/Hardware/rocketchip-zcu102.md b/Hardware/rocketchip-zcu102.md index 4d90174eec6..6be691931d9 100644 --- a/Hardware/rocketchip-zcu102.md +++ b/Hardware/rocketchip-zcu102.md @@ -2,12 +2,12 @@ riscv_hardware: true cmake_plat: rocketchip-zcu102 xcompiler_arg: -DRISCV64=1 -platform: Rocketchip +platform: Rocketchip (zcu102) arch: RV64IMAFDC virtualization: false iommu: false simulation_target: false -verification: [] +verification: [RISCV64] Contrib: 'DornerWorks' Maintained: 'DornerWorks' cpu: Rocket diff --git a/Hardware/rocketchip.md b/Hardware/rocketchip.md index 3f9dd82b31f..52e75312782 100644 --- a/Hardware/rocketchip.md +++ b/Hardware/rocketchip.md @@ -7,7 +7,7 @@ arch: RV64IMAFDC virtualization: false iommu: false simulation_target: false -verification: [] +verification: [RISCV64] Contrib: Data61 Maintained: seL4 Foundation cpu: Rocket diff --git a/Hardware/spike.md b/Hardware/spike.md index 907169ec712..bf08ac886c7 100644 --- a/Hardware/spike.md +++ b/Hardware/spike.md @@ -7,6 +7,7 @@ arch: RV32GC, RV64IMAFDC virtualization: false iommu: false simulation_target: true +simulation_only: true verification: [] Contrib: 'Data61, Hesham Almatary' Maintained: "seL4 Foundation" diff --git a/projects/sel4/verified-configurations.md b/projects/sel4/verified-configurations.md index e0d38f1c56b..691fb3f1356 100644 --- a/projects/sel4/verified-configurations.md +++ b/projects/sel4/verified-configurations.md @@ -29,23 +29,28 @@ Current verified configurations can be found in seL4 sources in the ```sh cd configs/ ls *_verified.cmake -# AARCH64_bcm2711_verified.cmake ARM_exynos5410_verified.cmake -# AARCH64_hikey_verified.cmake ARM_exynos5422_verified.cmake -# AARCH64_imx8mm_verified.cmake ARM_hikey_verified.cmake -# AARCH64_imx8mq_verified.cmake ARM_HYP_exynos5_verified.cmake -# AARCH64_imx93_verified.cmake ARM_HYP_exynos5410_verified.cmake -# AARCH64_maaxboard_verified.cmake ARM_HYP_verified.cmake -# AARCH64_odroidc2_verified.cmake ARM_imx8mm_verified.cmake -# AARCH64_odroidc4_verified.cmake ARM_MCS_verified.cmake -# AARCH64_rockpro64_verified.cmake ARM_omap3_verified.cmake -# AARCH64_tqma_verified.cmake ARM_tk1_verified.cmake -# AARCH64_tx1_verified.cmake ARM_verified.cmake -# AARCH64_ultra96v2_verified.cmake ARM_zynq7000_verified.cmake -# AARCH64_verified.cmake ARM_zynqmp_verified.cmake -# AARCH64_zynqmp_verified.cmake RISCV64_MCS_verified.cmake -# ARM_am335x_verified.cmake RISCV64_verified.cmake -# ARM_bcm2837_verified.cmake X64_verified.cmake -# ARM_exynos4_verified.cmake +# AARCH64_bcm2711_verified.cmake ARM_hikey_verified.cmake +# AARCH64_bcm2712_verified.cmake ARM_HYP_exynos5_verified.cmake +# AARCH64_hikey_verified.cmake ARM_HYP_exynos5410_verified.cmake +# AARCH64_imx8mm_verified.cmake ARM_HYP_verified.cmake +# AARCH64_imx8mq_verified.cmake ARM_imx8mm_verified.cmake +# AARCH64_imx93_verified.cmake ARM_MCS_verified.cmake +# AARCH64_maaxboard_verified.cmake ARM_omap3_verified.cmake +# AARCH64_MCS_verified.cmake ARM_tk1_verified.cmake +# AARCH64_odroidc2_verified.cmake ARM_verified.cmake +# AARCH64_odroidc4_verified.cmake ARM_zynq7000_verified.cmake +# AARCH64_rockpro64_verified.cmake ARM_zynqmp_verified.cmake +# AARCH64_stm32mp2_verified.cmake RISCV64_ariane_verified.cmake +# AARCH64_tqma_verified.cmake RISCV64_bananapi-f3_verified.cmake +# AARCH64_tx1_verified.cmake RISCV64_cheshire_verified.cmake +# AARCH64_ultra96v2_verified.cmake RISCV64_hifive-p550_verified.cmake +# AARCH64_verified.cmake RISCV64_MCS_verified.cmake +# AARCH64_zynqmp_verified.cmake RISCV64_polarfire_verified.cmake +# ARM_am335x_verified.cmake RISCV64_rocketchip_verified.cmake +# ARM_bcm2837_verified.cmake RISCV64_rocketchip-zcu102_verified.cmake +# ARM_exynos4_verified.cmake RISCV64_star64_verified.cmake +# ARM_exynos5410_verified.cmake RISCV64_verified.cmake +# ARM_exynos5422_verified.cmake X64_verified.cmake ``` To obtain specific source code and build for a given configuration (e.g. @@ -73,10 +78,9 @@ At present, none of our verified configurations take into account address translation for devices (System MMU or IOMMU), debug/profiling/printing interfaces, or the kernel startup at boot. -The proofs for RISCV64\_MCS/ARM\_MCS (mixed-criticality extensions to real-time -seL4 features), as well as confidentiality proofs for AARCH64 are in progress. -Refer to the [roadmap](https://sel4.systems/roadmap.html) for status and -upcoming features. +The proofs for AARCH64\_MCS/ARM\_MCS (mixed-criticality extensions to real-time +seL4 features) are in progress. Refer to the +[roadmap](https://sel4.systems/roadmap.html) for status and upcoming features. ### Arm Aarch32 (`ARM`) {#ARM} From 1c5095b9470d48b63f42cc82997bfe531a231914 Mon Sep 17 00:00:00 2001 From: Gerwin Klein Date: Mon, 24 Aug 2026 11:54:13 +0200 Subject: [PATCH 2/2] verified configs: add AARCH64 confidentiality (now proved) Signed-off-by: Gerwin Klein --- projects/sel4/verified-configurations.md | 1 + 1 file changed, 1 insertion(+) diff --git a/projects/sel4/verified-configurations.md b/projects/sel4/verified-configurations.md index 691fb3f1356..e171ccae750 100644 --- a/projects/sel4/verified-configurations.md +++ b/projects/sel4/verified-configurations.md @@ -160,6 +160,7 @@ The following properties are verified: - C-level functional correctness, including fast path - integrity and availability (access control) +- confidentiality (information flow) Further properties are under development. See also the [roadmap](https://sel4.systems/roadmap.html) for status and schedule.