Add verified RISC-V platforms

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

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)

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

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

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

Hardware/polarfire.md

@@ -7,7 +7,7 @@ arch: RV64IMAC, RV64GC
 virtualization: false
 iommu: false
 simulation_target: false
-verification: []
+verification: [RISCV64]
 Contrib: '<a href="https://dornerworks.com">DornerWorks</a>'
 Maintained: '<a href="https://dornerworks.com">DornerWorks</a>'
 soc: PolarFire SoC FPGA

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: '<a href="https://dornerworks.com">DornerWorks</a>'
 Maintained: '<a href="https://dornerworks.com">DornerWorks</a>'
 cpu: Rocket

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

Hardware/spike.md

@@ -7,6 +7,7 @@ arch: RV32GC, RV64IMAFDC
 virtualization: false
 iommu: false
 simulation_target: true
+simulation_only: true
 verification: []
 Contrib: 'Data61, <a href="https://github.com/heshamelmatary">Hesham Almatary</a>'
 Maintained: "seL4 Foundation"

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}
 
@@ -156,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.