From 96b379ca4f5de30e059bdd433eba5f68135955d5 Mon Sep 17 00:00:00 2001 From: Gerwin Klein Date: Thu, 28 Mar 2024 20:11:45 -0400 Subject: [PATCH] roadmap: update AARCH64 and Multikernel status - remove multikernel item as completed (new mk item to be added when funding is available) - update AARCH64 status to FC complete, integrity ongoing - update TX2 board status Signed-off-by: Gerwin Klein --- Hardware/JetsonTX2.md | 2 +- _data/projects/l4v.yml | 10 ++-------- projects/sel4/verified-configurations.md | 6 +++--- 3 files changed, 6 insertions(+), 12 deletions(-) diff --git a/Hardware/JetsonTX2.md b/Hardware/JetsonTX2.md index 5d2a88dfc0..f20e178cfd 100644 --- a/Hardware/JetsonTX2.md +++ b/Hardware/JetsonTX2.md @@ -9,7 +9,7 @@ virtualization: "Yes" iommu: "Yes" soc: NVIDIA Tegra X2 cpu: Cortex-A57 Quad, Dual NVIDIA Denver -Status: "[Ongoing](/projects/sel4/verified-configurations.html#aarch64)" +Status: "FC complete, [Integrity ongoing](/projects/sel4/verified-configurations.html#aarch64)" Contrib: Data61 Maintained: seL4 Foundation SPDX-License-Identifier: CC-BY-SA-4.0 diff --git a/_data/projects/l4v.yml b/_data/projects/l4v.yml index f75be5d02a..9d7d7b3378 100644 --- a/_data/projects/l4v.yml +++ b/_data/projects/l4v.yml @@ -25,13 +25,7 @@ roadmap: roadmap_type: in-progress - name: AARCH64 display_name: AArch64 port - description: Functional correctness proofs for the AArch64 port of seL4. + description: Functional correctness proofs for the AArch64 port of seL4 completed. Integrity (access control) ongoing. assigned: Proofcraft - status: C verification to complete Q1/24 - roadmap_type: in-progress - - name: Multikernel - display_name: Multikernel - description: Functional correctness proofs for static multikernel config of seL4. - assigned: Proofcraft - status: concurrency framework ongoing + status: Integrity verification to complete Q1/25 roadmap_type: in-progress diff --git a/projects/sel4/verified-configurations.md b/projects/sel4/verified-configurations.md index 1757624907..a4633b443f 100644 --- a/projects/sel4/verified-configurations.md +++ b/projects/sel4/verified-configurations.md @@ -65,8 +65,8 @@ address translation for devices (System MMU or IOMMU), debug/profiling 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 proofs for AARCH64 are in progress. Refer to the -[roadmap](/projects/roadmap.html) for status and upcoming features. +seL4 features), as well as security proofs for AARCH64 are in progress. Refer to +the [roadmap](/projects/roadmap.html) for status and upcoming features. ## ARM Sabre Lite @@ -121,7 +121,7 @@ Mixed-Criticality-Systems API | Yes | Platform | Tegra X2 (Jetson TX2) | Floating-point support | Yes | Hypervisor mode | Yes -| **Verified properties** | in progress +| **Verified properties** | functional correctness, incl fast path completed; integrity proof in progress ## RISCV64