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, not that the feature support is limited by the simulator.

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
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 BCM2937 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
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