Supported Platforms
Verification status
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.
Simulating seL4
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.
x86
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 |
ARM
seL4 has support for select ARMv7 and ARMv8 Platforms.
| Platform | System-on-chip | Core | Arch | Virtualisation | IOMMU | Status | Contributed by | Maintained by |
|---|---|---|---|---|---|---|---|---|
| Arndale | Exynos5 | Cortex-A15 | ARMv7A | ARM Hyp | No | Unverified | Data61 | No |
| 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 | Unverified | Data61 | seL4 Foundation |
| Imx8mm | IMX8MM-EVK | Cortex-A53 Quad 1.8 GHz | ARMv8A, AArch64 | No | No | FC | Data61 | seL4 Foundation |
| Inforce IFC6410 | Snapdragon S4 Pro APQ8064 | Krait (Cortex-A15 like) | ARMv7A | No | No | Unverified | Data61 | No |
| Odroid-C2 | Amlogic S905 | Cortex-A53 | ARMv8A, AArch64 only | No | No | Unverified | Data61 | seL4 Foundation |
| Odroid-C4 | Amlogic S905X3 | Cortex-A55 | ARMv8A, AArch64 only | Yes | No | Unverified | Data61 | seL4 Foundation |
| OdroidX | Exynos4412 | Cortex-A9 | ARMv7A | No | No | Unverified | Data61 | seL4 Foundation |
| OdroidXU | Exynos5 | Cortex-A15 | ARMv7A | ARM HYP | limited System MMU | Unverified | Data61 | seL4 Foundation |
| OdroidXU4 | Exynos5 | Cortex-A15 | ARMv7A | ARM HYP | limited System MMU | 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 4-b | BCM2711 | Cortex-A72 | ARMv8A | ARM HYP | No | Unverified | 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 | System MMU | Unverified | Data61 | seL4 Foundation |
| TK1-SOM | NVIDIA Tegra K1 | Cortex-A15 | ARMv7A | ARM HYP | System MMU | FC with HYP, no SMMU | Data61 | seL4 Foundation |
| TX1 | NVIDIA Tegra X1 | Cortex-A57 Quad | ARMv8A, AArch64 only | ARM HYP | System MMU | Unverified | Data61 | seL4 Foundation |
| TX2 | NVIDIA Tegra X2 | Cortex-A57 Quad, Dual NVIDIA Denver | ARMv8A, AArch64 only | Yes | Yes | in progress | Data61 | seL4 Foundation |
| Ultra96v2 Evaluation Kit | Zynq UltraScale+ MPSoC | Cortex-A53 | ARMv8A | ARM HYP | System MMU | Unverified | DornerWorks | DornerWorks |
| Zynq ZCU102 and ZCU106 Evaluation Kits | Zynq UltraScale+ MPSoC | Cortex-A53 | ARMv8A | ARM HYP | System MMU | Unverified | DornerWorks | DornerWorks |
| Zynq-7000 ZC706 Evaluation Kit | Zynq7000 | Cortex-A9 | ARMv7A | No | No | Unverified | 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 | Status | Contributed by | Maintained by |
| Ariane | No | Ariane | RV64IMAC | No | Pending | Data61 | Hensoldt Cyber | |
| 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 |