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 | FC (without VT-X, VT-D and fastpath) | 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 |