SPDX-License-Identifier | SPDX-FileCopyrightText |
---|---|
CC-BY-SA-4.0 |
2020 seL4 Project a Series of LF Projects, LLC. |
The seL4 proofs are only for specific platforms, as noted in the Status column as follows:
- Unverified: this platform is not verified at all and is not scheduled for verification.
- Pending: 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.
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.
See Running It for how to run seL4 using Qemu.
We support PC99-style Intel Architecture Platforms.
Platform | Arch | Virtualisation | IOMMU | Status | Contributed by | Maintained by |
---|---|---|---|---|---|---|
PC99 (32-bit) | x86 | VT-X | VT-D | Unverified | Data61 | seL4 Foundation |
PC99 (64-bit) | x64 | VT-X | VT-D | FC (without VT-X, VT-D and fastpath) | Data61 | seL4 Foundation |
seL4 has support for select ARMv7 and ARMv8 Platforms.
Platform | System-on-chip | Core | Arch | Virtualisation | IOMMU | Status | Contributed by | Maintained by |
---|---|---|---|---|---|---|---|---|
{%- assign sorted = site.pages | sort: 'platform' %} | |||||||
{% for page in sorted %} | ||||||||
{%- if page.arm_hardware -%} | ||||||||
{{ page.platform }} | {{ page.soc}} | {{ page.cpu }} | {{ page.arch }} | {{ page.virtualization }} | {{ page.iommu}} | {{ page.Status }} | {{ page.Contrib }} | {{page.Maintained}} |
{% endif %} | ||||||||
{%- endfor %} |
We currently provide support for some of the RISC-V platforms. Support for the hypervisor extension is yet to be mainlined.
| Platform | Simulation | System-on-chip | Core | Arch | Virtualisation | Status | Contributed by | Maintained by | {% for page in sorted %} {%- if page.riscv_hardware -%} | {{ page.platform }} | {% if page.simulation_target %}Yes{% else %}No{% endif %} | {{ page.soc }} | {{ page.cpu }} | {{ page.arch }} | {{ page.virtualization }} | {{ page.Status }} | {{ page.Contrib }} | {{ page.Maintained }} | {% endif %} {%- endfor %}