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 verfied 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 infoflow.

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 Data61
PC99 (64-bit) x64 VT-X VT-D Pending Data61 Data61

ARM

seL4 has support for select ARMv6, ARMv7 and ARMv8 Platforms.

Platform System-on-chip Core Arch Virtualisation IOMMU Status Contributed by Maintained by
KZM i.MX31 ARM1136J ARMv6A No No Unverified Data61 Data61
BeagleBoard OMAP3 Cortex-A8 ARMv7A No No Unverified Data61 Data61
Beaglebone Black AM335x Cortex-A8 ARMv7A No No Unverified Community Data61
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 Data61
OdroidXU4 Exynos5 Cortex-A15 ARMv7A ARM HYP limited System MMU Unverified Data61 Data61
Zynq-7000 ZC706 Evaluation Kit Zynq7000 Cortex-A9 ARMv7A No No Unverified Data61 Data61
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 Data61
TK1 NVIDIA Tegra K1 Cortex-A15 ARMv7A ARM HYP System MMU Unverified Data61 Data61
OdroidX Exynos4412 Cortex-A9 ARMv7A No No Unverified Data61 Data61
Sabre Lite i.MX6 Cortex-A9 ARMv7A No No Verified Data61 Data61
Raspberry Pi 3-b BCM2837 Cortex-A53 ARMv8A ARM HYP No Unverified Data61 Data61
Zynq ZCU102 Evaluation Kit Zynq UltraScale+ MPSoC Cortex-A53 ARMv8A ARM HYP System MMU Unverified DornerWorks DornerWorks
HiKey Kirin 620 Cortex-A53 ARMv8A ARM HYP No Unverified Data61 Data61
TX2 NVIDIA Tegra X2 Cortex-A57 Quad, Dual NVIDIA Denver ARMv8A, AArch64 only No No Unverified Data61 Data61
TX1 NVIDIA Tegra X1 Cortex-A57 Quad ARMv8A, AArch64 only ARM HYP System MMU Unverified Data61 Data61

RISC-V

We currently provide a prototype support for the 64-bit RISC-V spike platform. See Simulating RISC-V. Multicore and the floating point unit (FPU) are not supported.

platform (board) status cotributed by maintained by
Spike Unverified Data61, Hesham Almatary Data61