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 <[email protected]>
seL4 · Mar 29, 2024 · 96b379c · 96b379c
1 parent 03d2420
commit 96b379c
Show file tree

Hide file tree

Showing 3 changed files with 6 additions and 12 deletions.
diff --git 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
@@ -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
@@ -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