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
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 Unverified 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
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 Unverified 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 (without MMU) 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 Unverified Data61 seL4 Foundation
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. 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
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
Spike Yes     RV32GC, RV64IMAFDC No Unverified Data61, Hesham Almatary seL4 Foundation