From 183b465e8e6c83f6efbcff85dac7eab9e1a05b1b Mon Sep 17 00:00:00 2001 From: Gerwin Klein Date: Mon, 11 Sep 2023 18:44:28 +0200 Subject: [PATCH] update verified platforms; adjust links Signed-off-by: Gerwin Klein --- Hardware/CEI_TK1_SOM/index.md | 2 +- Hardware/OdroidXU4.md | 2 +- Hardware/imx8mm.md | 2 +- Hardware/sabreLite.md | 2 +- projects/sel4/verified-configurations.md | 22 ++++++++++++++++++++-- 5 files changed, 24 insertions(+), 6 deletions(-) diff --git a/Hardware/CEI_TK1_SOM/index.md b/Hardware/CEI_TK1_SOM/index.md index 9eaaccedd5..fe416df32e 100644 --- a/Hardware/CEI_TK1_SOM/index.md +++ b/Hardware/CEI_TK1_SOM/index.md @@ -8,7 +8,7 @@ virtualization: ARM HYP iommu: System MMU soc: NVIDIA Tegra K1 cpu: Cortex-A15 -Status: "[FC (without System MMU)](/projects/sel4/verified-configurations.html#arm_hyp)" +Status: "[FC with HYP, no SMMU](/projects/sel4/verified-configurations.html#arm_hyp-tk1)" Contrib: Data61 Maintained: seL4 Foundation SPDX-License-Identifier: CC-BY-SA-4.0 diff --git a/Hardware/OdroidXU4.md b/Hardware/OdroidXU4.md index 8ce9df7e51..52f8339bb9 100644 --- a/Hardware/OdroidXU4.md +++ b/Hardware/OdroidXU4.md @@ -8,7 +8,7 @@ virtualization: ARM HYP iommu: limited System MMU soc: Exynos5 cpu: Cortex-A15 -Status: FC with HYP, no System MMU +Status: "[FC with HYP, no SMMU](/projects/sel4/verified-configurations.html#arm_hyp-exynos5)" Contrib: Data61 Maintained: seL4 Foundation SPDX-License-Identifier: CC-BY-SA-4.0 diff --git a/Hardware/imx8mm.md b/Hardware/imx8mm.md index d7ea1f3599..9f81a96795 100644 --- a/Hardware/imx8mm.md +++ b/Hardware/imx8mm.md @@ -9,7 +9,7 @@ virtualization: "No" iommu: "No" soc: IMX8MM-EVK cpu: Cortex-A53 Quad 1.8 GHz -Status: "FC" +Status: "[FC](/projects/sel4/verified-configurations.html#arm-imx8-mm)" Contrib: Data61 Maintained: seL4 Foundation SPDX-License-Identifier: CC-BY-SA-4.0 diff --git a/Hardware/sabreLite.md b/Hardware/sabreLite.md index 30e2c076e7..5fba6310f3 100644 --- a/Hardware/sabreLite.md +++ b/Hardware/sabreLite.md @@ -9,7 +9,7 @@ virtualization: "No" iommu: "No" soc: i.MX6 cpu: Cortex-A9 -Status: "[Verified](/projects/sel4/verified-configurations.html#arm)" +Status: "[Verified](/projects/sel4/verified-configurations.html#arm-sabre-lite)" Contrib: Data61 Maintained: seL4 Foundation SPDX-License-Identifier: CC-BY-SA-4.0 diff --git a/projects/sel4/verified-configurations.md b/projects/sel4/verified-configurations.md index 8056f32c12..94cfb5be9c 100644 --- a/projects/sel4/verified-configurations.md +++ b/projects/sel4/verified-configurations.md @@ -67,7 +67,7 @@ The proofs for RISCV64\_MCS/ARM\_MCS (mixed-criticality extensions to real-time seL4 features), as well as proofs for AARCH64 are in progress. Refer to the [roadmap](/projects/roadmap.html) for status and upcoming features. -## ARM +## ARM Sabre Lite | File | `ARM_verified.cmake` | Architecture | ARMv7 @@ -76,6 +76,15 @@ seL4 features), as well as proofs for AARCH64 are in progress. Refer to the | Hypervisor mode | No | **Verified properties** | functional correctness incl fast path, integrity (access control), confidentiality (information flow), binary correctness (covers all verified C code), user-level system initialisation +## ARM iMX8 MM + +| File | `ARM_imx8mm_verified.cmake` +| Architecture | ARMv7 +| Platform | IMX8MM-EVK +| Floating-point support | Yes +| Hypervisor mode | No +| **Verified properties** | functional correctness incl fast path + ## ARM_MCS File | `ARM_MCS_verified.cmake` @@ -86,7 +95,7 @@ Hypervisor mode | No Mixed-Criticality-Systems API | Yes **Verified properties** | in progress (design-level functional correctness completed) -## ARM\_HYP +## ARM\_HYP TK1 File | `ARM_HYP_verified.cmake` Architecture | ARMv7 @@ -95,6 +104,15 @@ Floating-point support | No Hypervisor mode | Yes **Verified properties** | functional correctness, incl fast path +## ARM\_HYP Exynos5 + +File | `ARM_HYP_exynos5_verified.cmake` +Architecture | ARMv7 +Platform | Odroid XU4 +Floating-point support | No +Hypervisor mode | Yes +**Verified properties** | functional correctness, incl fast path + ## AARCH64 | File | `AARCH64_verified.cmake`