From 94d415117e5ab747a93841a2d0c8c04c8581be00 Mon Sep 17 00:00:00 2001 From: June Andronick Date: Wed, 20 Dec 2023 17:53:30 +0100 Subject: [PATCH] hardware: improve the text (#216) * 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 Co-authored-by: Gerwin Klein --- Hardware/index.md | 37 +++++++++++++++++++++++++++++++------ 1 file changed, 31 insertions(+), 6 deletions(-) diff --git a/Hardware/index.md b/Hardware/index.md index fdc64481f8..024880b557 100644 --- a/Hardware/index.md +++ b/Hardware/index.md @@ -4,23 +4,48 @@ 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 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. + + +### Platforms' attributes + +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)); +- who has contributed this platform port; +- who is maintaining this platform port. + +### 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