From a59ceb31d624eebd736108044f2b90f947bcda93 Mon Sep 17 00:00:00 2001 From: June Andronick <june.andronick@proofcraft.systems> Date: Tue, 19 Dec 2023 15:30:41 +0100 Subject: [PATCH 1/4] hardware: improve the text - added a high-level summary - added a description of the table - added a link to the verified configuration page - small language tweaks Signed-off-by: June Andronick <june.andronick@proofcraft.systems> --- Hardware/index.md | 36 ++++++++++++++++++++++++++++++------ 1 file changed, 30 insertions(+), 6 deletions(-) diff --git a/Hardware/index.md b/Hardware/index.md index fdc64481f84..14cca52fb20 100644 --- a/Hardware/index.md +++ b/Hardware/index.md @@ -4,23 +4,47 @@ SPDX-FileCopyrightText: 2020 seL4 Project a Series of LF Projects, LLC. --- # Supported Platforms -## Verification status +### Summary -The seL4 proofs are only for specific platforms, as noted in the *Status* column as follows: +seL4 is available on 3 major hardware architectures, [ARM](#arm), +[RISC-V](#risc-v) and [x86](#x86), for a number of platforms (with varying +hardware features). + +seL4 is formally verified (to various degrees) for a subset of these +configurations, i.e. combination of architecture, platform and hardware +features. + +Details are given in the tables below. + +### Platforms' attributes + +The tables below list of all the platforms for which seL4's implementation is +available. For each platform, the tables list: + +- whether specific features are supported (e.g. *Virtualisation*, *IOMMU/SSMU*, etc) and to which degree (where applicable); +- the *verification status* (see more [below](#verification-status)); +- who has contributed this configuration; +- who is maintaining this configuration. + +### Verification status + +The seL4 proofs only hold for specific configurations, as noted in the *Verification Status* column in the tables, as follows: * Unverified: this platform is not verified at all and is not scheduled for verification. * Ongoing: this feature is currently undergoing verification. * FC: the functional correctness proofs are complete. * Verified: all proofs for this platform are complete, including functional correctness, integrity and information flow. -## Simulating seL4 +More information can be found on the [Verified Configurations](../projects/sel4/verified-configurations.md) page. + -Running seL4 in a simulator is a quick way to test it out and iteratively develop software. However, -note that feature support is limited by the simulator. +### Simulating seL4 +Running seL4 in a simulator is a quick way to test it out and iteratively develop software. +Note that feature support is then limited by the simulator. See [Running It](/seL4Test#RunningIt) for how to run seL4 using Qemu. -* [Running seL4 on VMware](VMware) +You can also [run seL4 on VMware](VMware). ## x86 From 414776d9286166886d05718e83087b228e26145c Mon Sep 17 00:00:00 2001 From: June Andronick <june.andronick@proofcraft.systems> Date: Wed, 20 Dec 2023 17:39:55 +0100 Subject: [PATCH 2/4] hardware: feedback from Gerwin Co-authored-by: Gerwin Klein <gerwin.klein@proofcraft.systems> Signed-off-by: June Andronick <june.andronick@proofcraft.systems> --- Hardware/index.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Hardware/index.md b/Hardware/index.md index 14cca52fb20..ce0fbd5baa9 100644 --- a/Hardware/index.md +++ b/Hardware/index.md @@ -7,8 +7,8 @@ SPDX-FileCopyrightText: 2020 seL4 Project a Series of LF Projects, LLC. ### Summary seL4 is available on 3 major hardware architectures, [ARM](#arm), -[RISC-V](#risc-v) and [x86](#x86), for a number of platforms (with varying -hardware features). +[RISC-V](#risc-v) and [x86](#x86), for a number of platforms with varying +hardware features. seL4 is formally verified (to various degrees) for a subset of these configurations, i.e. combination of architecture, platform and hardware From 342fd87c5a822cfb25412f2ca3f71a0f1bc6fff7 Mon Sep 17 00:00:00 2001 From: June Andronick <june.andronick@proofcraft.systems> Date: Wed, 20 Dec 2023 17:40:10 +0100 Subject: [PATCH 3/4] hardware: feedback from Gerwin Co-authored-by: Gerwin Klein <gerwin.klein@proofcraft.systems> Signed-off-by: June Andronick <june.andronick@proofcraft.systems> --- Hardware/index.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Hardware/index.md b/Hardware/index.md index ce0fbd5baa9..0e28c73a170 100644 --- a/Hardware/index.md +++ b/Hardware/index.md @@ -23,8 +23,8 @@ available. For each platform, the tables list: - whether specific features are supported (e.g. *Virtualisation*, *IOMMU/SSMU*, etc) and to which degree (where applicable); - the *verification status* (see more [below](#verification-status)); -- who has contributed this configuration; -- who is maintaining this configuration. +- who has contributed this platform port; +- who is maintaining this platform port. ### Verification status From c2423cc79af54ae7000faf0b6d87593aedb37b5b Mon Sep 17 00:00:00 2001 From: June Andronick <june.andronick@proofcraft.systems> Date: Wed, 20 Dec 2023 17:46:15 +0100 Subject: [PATCH 4/4] hardware: feedback from Gerwin Signed-off-by: June Andronick <june.andronick@proofcraft.systems> --- Hardware/index.md | 13 +++++++------ 1 file changed, 7 insertions(+), 6 deletions(-) diff --git a/Hardware/index.md b/Hardware/index.md index 0e28c73a170..024880b5570 100644 --- a/Hardware/index.md +++ b/Hardware/index.md @@ -10,16 +10,17 @@ seL4 is available on 3 major hardware architectures, [ARM](#arm), [RISC-V](#risc-v) and [x86](#x86), for a number of platforms with varying hardware features. -seL4 is formally verified (to various degrees) for a subset of these -configurations, i.e. combination of architecture, platform and hardware -features. +seL4 is formally verified for specific configurations for a subset of these +platforms. The depth of the proofs and which properties are verified depend on +the platform. + +The tables below provide more details. -Details are given in the tables below. ### Platforms' attributes -The tables below list of all the platforms for which seL4's implementation is -available. For each platform, the tables list: +The tables below list the platforms for which seL4 is available. For each +platform, the tables list: - whether specific features are supported (e.g. *Virtualisation*, *IOMMU/SSMU*, etc) and to which degree (where applicable); - the *verification status* (see more [below](#verification-status));