Supported Platforms
Verification status
The seL4 proofs are only for specific platforms, as noted in the tables for x86 and ARM below, 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.
- FCI: the integrity proofs are complete, in addition to functional correctness.
- 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 ARMv6, ARMv7 and ARMv8 Platforms.
| Platform | System-on-chip | Core | Arch | Virtualisation | IOMMU | Status | Contributed by | Maintained by |
|---|---|---|---|---|---|---|---|---|
| BeagleBoard | OMAP3 | Cortex-A8 | ARMv7A | No | No | Unverified | Data61 | seL4 Foundation |
| BeagleBone Black / Blue | AM335x | Cortex-A8 | ARMv7A | No | No | Unverified | Community | seL4 Foundation |
| Inforce IFC6410 | Snapdragon S4 Pro APQ8064 | Krait (Cortex-A15 like) | ARMv7A | No | No | Unverified | Data61 | No |
| OdroidXU | Exynos5 | Cortex-A15 | ARMv7A | ARM HYP | limited System MMU | Unverified | Data61 | seL4 Foundation |
| OdroidXU4 | Exynos5 | Cortex-A15 | ARMv7A | ARM HYP | limited System MMU | Unverified | Data61 | seL4 Foundation |
| Zynq-7000 ZC706 Evaluation Kit | Zynq7000 | Cortex-A9 | ARMv7A | No | No | Unverified | Data61 | seL4 Foundation |
| Arndale | Exynos5 | Cortex-A15 | ARMv7A | ARM Hyp | No | Unverified | Data61 | No |
| TK1-SOM | NVIDIA Tegra K1 | Cortex-A15 | ARMv7A | ARM HYP | System MMU | FC (without MMU) | Data61 | seL4 Foundation |
| TK1 | NVIDIA Tegra K1 | Cortex-A15 | ARMv7A | ARM HYP | System MMU | Unverified | Data61 | seL4 Foundation |
| OdroidX | Exynos4412 | Cortex-A9 | ARMv7A | No | No | Unverified | Data61 | seL4 Foundation |
| Sabre Lite | i.MX6 | Cortex-A9 | ARMv7A | No | No | Verified | 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 |
| Zynq ZCU102 and ZCU106 Evaluation Kits | Zynq UltraScale+ MPSoC | Cortex-A53 | ARMv8A | ARM HYP | System MMU | Unverified | DornerWorks | DornerWorks |
| imx8mq | MCIMX8M-EVKB | Cortex-A53 Quad 1.5 GHz | ARMv8A | No | No | Unverified | Data61 | 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 | Unverified | Data61 | seL4 Foundation |
| Rockpro64 | RK3399 hexa-core | Cortex-A53 Quad 1.8 GHz | ARMv8A, AArch64 | No | No | Unverified | Data61 | seL4 Foundation |
| TX2 | NVIDIA Tegra X2 | Cortex-A57 Quad, Dual NVIDIA Denver | ARMv8A, AArch64 only | No | No | Unverified | Data61 | seL4 Foundation |
| Odroid-C2 | Amlogic S905 | Cortex-A53 | ARMv8A, AArch64 only | No | No | Unverified | Data61 | seL4 Foundation |
| TX1 | NVIDIA Tegra X1 | Cortex-A57 Quad | ARMv8A, AArch64 only | ARM HYP | System MMU | Unverified | Data61 | seL4 Foundation |
RISC-V
We currently provide support for some of the RISC-V platforms. Multicore, floating point unit (FPU) and hypervisor extension support are under internal review, will be released soon.
| Platform | Simulation | System-on-chip | Core | Arch | Virtualisation | Status | Contributed by | Maintained by |
| Spike | Yes | RV32GC, RV64IMAFDC | No | Unverified | Data61, Hesham Almatary | seL4 Foundation | ||
| Ariane | No | Ariane | RV64IMAC | No | Pending | Data61 | Hensoldt Cyber | |
| HiFive Unleashed | No | Freedom U540 | U54-MC, E51 | RV64IMAC, RV64GC | No | FC | Data61 | seL4 Foundation |
| Rocketchip | No | Rocket | RV64IMAFDC | No | Unverified | Data61 | seL4 Foundation |