Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

update status of verified configs #198

Merged
merged 2 commits into from
Sep 14, 2023
Merged

update status of verified configs #198

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
9a955e0
mark imx8mm and odroidxu4 as verified
lsf37 Sep 11, 2023
d6246ea
update verified platforms; adjust links
lsf37 Sep 11, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion Hardware/CEI_TK1_SOM/index.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
2 changes: 1 addition & 1 deletion Hardware/OdroidXU4.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,7 @@ virtualization: ARM HYP
iommu: limited System MMU
soc: Exynos5
cpu: Cortex-A15
Status: Unverified
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
Expand Down
2 changes: 1 addition & 1 deletion Hardware/imx8mm.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -9,7 +9,7 @@ virtualization: "No"
iommu: "No"
soc: IMX8MM-EVK
cpu: Cortex-A53 Quad 1.8 GHz
Status: "FC, unmaintained"
Status: "[FC](/projects/sel4/verified-configurations.html#arm-imx8mm-evk)"
Contrib: Data61
Maintained: seL4 Foundation
SPDX-License-Identifier: CC-BY-SA-4.0
Expand Down
2 changes: 1 addition & 1 deletion Hardware/sabreLite.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
28 changes: 23 additions & 5 deletions projects/sel4/verified-configurations.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -67,26 +67,35 @@ 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
| Platform | iMX.6 (e.g. Sabre Lite)
| Platform | i.MX 6 (Sabre Lite)
| Floating-point support | No
| 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 IMX8MM-EVK

| 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`
Architecture | ARMv7
Platform | iMX.6 (e.g. Sabre Lite)
Platform | i.MX 6 (Sabre Lite)
Floating-point support | No
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
Expand All @@ -95,11 +104,20 @@ 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`
| Architecture | ARMv8
| Platform | Tegra X2 (e.g. Jetson TX2)
| Platform | Tegra X2 (Jetson TX2)
| Floating-point support | Yes
| Hypervisor mode | Yes
| **Verified properties** | in progress
Expand Down