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 | ARM11 | v6 | No | No | Unverified | Data61 | Data61 |
| Arndale | Exynos5 | A15 | v7A | ARM HYP | No | Unverified | Data61 | No |
| BeagleBoard | OMAP3 | A8 | v7A | No | No | Unverified | Data61 | Data61 |
| Beaglebone Black | AM335x | A8 | v7A | No | No | Unverified | external | Data61 |
| Inforce IFC6410 | Snapdragon S4 Pro APQ8064 | krait (A15-like) | v7A | ARM HYP | - | Unverified | Data61 | No |
| Jetson TK1 (NVIDIA) | Tegra K1 | A15 | v7-1A | ARM HYP | System MMU | Unverified | Data61 | Data61 |
| Odroid-X | Exynos4412 | A9 | v7A | No | No | Unverified | Data61 | Data61 |
| Odroid-XU | Exynos5 | A15 | v7A | ARM HYP | limited System MMU | Unverified | Data61 | Data61 |
| Sabre Lite | i.MX6 | A9 | v7A | No | No | Verified | Data61 | Data61 |
| TK1 SOM (Colorado Engineering) | Tegra K1 | A15 | v7-1A | ARM HYP | System MMU | FC (without MMU) | Data61 | Data61 |
| Zynq-7000 ZC706 Evaluation Kit | Zynq 7000 | A9 | v7A | No | No | Unverified | Data61 | Data61 |
| Zynq ZCU102 Evaluation Kit | Zynq !UltraScale+ MPSoC | A53 | v8A | ARM HYP | System MMU | Unverified | DornerWorks | Data61 |
| Jetson TX1 (NVIDIA) | Tegra X1 | Quad A57 | v8A, aarch64 | ARM HYP | System MMU | Unverified | Data61 | Data61 |
| HiKey | Kirin 620 | A53 | v8A, aarch32 & aarch64 | ARM HYP | - | Unverified | Data61 | Data61 |
| Raspberry Pi 3-b | BCM2837 | A53 | v8A aarch64 | ARM HYP | - | 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 |