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

hardware: improve the text #216

Merged
merged 4 commits into from
Dec 20, 2023
Merged

hardware: improve the text #216

Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
a59ceb3
hardware: improve the text
june-andronick Dec 19, 2023
414776d
hardware: feedback from Gerwin
june-andronick Dec 20, 2023
342fd87
hardware: feedback from Gerwin
june-andronick Dec 20, 2023
c2423cc
hardware: feedback from Gerwin
june-andronick Dec 20, 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
37 changes: 31 additions & 6 deletions Hardware/index.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down