Supported platforms
Summary
seL4 is available on 3 major hardware architectures, ARM, RISC-V and 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/SMMU, etc) and to which degree (where applicable);
- the verification status (see more below);
- 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.
More information can be found on the Verified Configurations page.
Not in the lists below?
If the platform, architecture, feature that you are after is not listed on this page, you have several options, listed below. It is important to note however that, as explained in the guidelines linked below, contributing new ports or features will require compelling arguments, discussion with the technical community (including through Request-For-Comments), as well as testing requirements and maintenance/expertise commitment, to a degree depending on the nature of the contribution.
-
You can contact one of the seL4 Foundation Endorsed Services Providers to get commercial support or professional advice to develop such a port or feature (with the implications and expectations detailed in our guidelines for contributing kernel code);
-
You can check the roadmap for any planned contributions, from the seL4 Foundation or larger community, such on any new architecture ports, new large formal verifications, or large or fundamental new features;
-
You can contact the seL4 community through one of our communication channels to ask whether someone is developing such a port or feature already, or whether there is general interest in discussing such a new port or feature;
-
If you are in a position to develop the seL4 port or feature yourself, you should follow our guidelines for contributing kernel code, which details the implications and expectations.
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 for how to run seL4 using Qemu.
You can also run seL4 on VMware.
ARM
seL4 has support for select ARMv7 and ARMv8 Platforms.
| Platform | System-on-chip | Core | Arch | Virtualisation | SMMU | Verification Status | Contributed by | Maintained by |
|---|---|---|---|---|---|---|---|---|
| Avnet MaaXBoard | i.MX8MQ | Cortex-A53 Quad 1.5 GHz | ARMv8A | No | No | Unverified | Capgemini Engineering | Capgemini Engineering |
| BeagleBoard | OMAP3 | Cortex-A8 | ARMv7A | No | No | Unverified | Data61 | seL4 Foundation |
| BeagleBone Black / Blue | AM335x | Cortex-A8 | ARMv7A | No | No | Unverified | Community | seL4 Foundation |
| HiKey | Kirin 620 | Cortex-A53 | ARMv8A | ARM HYP | No | Verified | Data61 | seL4 Foundation |
| Imx8mm | IMX8MM-EVK | Cortex-A53 Quad 1.8 GHz | ARMv8A, AArch64 | No | No | FC | Data61 | seL4 Foundation |
| Odroid-C2 | Amlogic S905 | Cortex-A53 | ARMv8A, AArch64 only | No | No | FC complete, Integrity ongoing | Data61 | seL4 Foundation |
| Odroid-C4 | Amlogic S905X3 | Cortex-A55 | ARMv8A, AArch64 only | Yes | No | FC complete, Integrity ongoing | Data61 | seL4 Foundation |
| OdroidX | Exynos4412 | Cortex-A9 | ARMv7A | No | No | Verified | Data61 | seL4 Foundation |
| OdroidXU | Exynos5 | Cortex-A15 | ARMv7A | ARM HYP | limited SMMU | Verified | Data61 | seL4 Foundation |
| OdroidXU4 | Exynos5 | Cortex-A15 | ARMv7A | ARM HYP | limited SMMU | FC with HYP, no SMMU | Data61 | seL4 Foundation |
| Raspberry Pi 3-b | BCM2837 | Cortex-A53 | ARMv8A | ARM HYP | No | Unverified | Data61 | seL4 Foundation |
| Raspberry Pi 4B | BCM2711 | Cortex-A72 | ARMv8A | ARM HYP | No | FC complete, Integrity ongoing | Hensoldt and ARM Research IceCap | Hensoldt |
| Rockpro64 | RK3399 hexa-core | Cortex-A53 Quad 1.8 GHz | ARMv8A, AArch64 | No | No | Unverified | Data61 | seL4 Foundation |
| Sabre Lite | i.MX6 | Cortex-A9 | ARMv7A | No | No | Verified | Data61 | seL4 Foundation |
| TK1 | NVIDIA Tegra K1 | Cortex-A15 | ARMv7A | ARM HYP | SMMU | Verified | Data61 | seL4 Foundation |
| TK1-SOM | NVIDIA Tegra K1 | Cortex-A15 | ARMv7A | ARM HYP | SMMU | FC with HYP, no SMMU | Data61 | seL4 Foundation |
| TX1 | NVIDIA Tegra X1 | Cortex-A57 Quad | ARMv8A, AArch64 only | ARM HYP | SMMU | Unverified | Data61 | seL4 Foundation |
| TX2 | NVIDIA Tegra X2 | Cortex-A57 Quad, Dual NVIDIA Denver | ARMv8A, AArch64 only | Yes | Yes | FC complete, Integrity ongoing | Data61 | seL4 Foundation |
| Ultra96v2 Evaluation Kit | Zynq UltraScale+ MPSoC | Cortex-A53 | ARMv8A | ARM HYP | SMMU | Unverified | DornerWorks | DornerWorks |
| Zynq ZCU102 and ZCU106 Evaluation Kits | Zynq UltraScale+ MPSoC | Cortex-A53 | ARMv8A | ARM HYP | SMMU | FC complete, Integrity ongoing | DornerWorks | DornerWorks |
| Zynq-7000 ZC706 Evaluation Kit | Zynq7000 | Cortex-A9 | ARMv7A | No | No | Verified | Data61 | seL4 Foundation |
| imx8mq | MCIMX8M-EVKB | Cortex-A53 Quad 1.5 GHz | ARMv8A | No | No | Unverified | Data61 | seL4 Foundation |
RISC-V
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 | Verification Status | Contributed by | Maintained by |
|---|---|---|---|---|---|---|---|---|
| Ariane | No | Ariane | RV64IMAC | No | Unverified | Data61 | Hensoldt Cyber | |
| Cheshire | No | Cheshire | RV64IMAFDC | No | Unverified | UNSW | UNSW | |
| HiFive Unleashed | No | Freedom U540 | U54-MC, E51 | RV64IMAC, RV64GC | No | Verified | Data61 | seL4 Foundation |
| Microchip PolarFire Icicle Kit | No | PolarFire SoC FPGA | U54-MC, E51 | RV64IMAC, RV64GC | No | Unverified | DornerWorks | DornerWorks |
| Rocketchip | No | Rocket | RV64IMAFDC | Yes | Unverified | DornerWorks | DornerWorks | |
| Rocketchip | No | Rocket | RV64IMAFDC | No | Unverified | Data61 | seL4 Foundation | |
| Spike | Yes | RV32GC, RV64IMAFDC | No | Unverified | Data61, Hesham Almatary | seL4 Foundation |
x86
We support PC99-style Intel Architecture Platforms.
| Platform | Arch | Virtualisation | IOMMU | Verification 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 |
Unmaintained platforms
Unmaintained platforms are platforms for which code has been contributed, but this code is not or no longer tested and is unlikely to work. We list these here, because bringing an unmaintained platform up may be faster and easier than starting from scratch on a new platform port.
ARM
| Platform | System-on-chip | Core | Arch | Virtualisation | SMMU | Verification Status | Contributed by |
|---|---|---|---|---|---|---|---|
| Arndale (unmaintained) | Exynos5 | Cortex-A15 | ARMv7A | ARM HYP | No | Unverified | Data61 |
| Inforce IFC6410 (unmaintained) | Snapdragon S4 Pro APQ8064 | Krait (Cortex-A15 like) | ARMv7A | No | No | Unverified | Data61 |