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 |