Diff: substrate/sel4-aarch64-qemu-substrate-target.es

From 06b1da5 to 06b1da5

+0 / −0 lines
BeforeAfter
--- ---
schema: foundry-doc-v1 schema: foundry-doc-v1
title: "The seL4 AArch64 QEMU Substrate Target" title: "The seL4 AArch64 QEMU Substrate Target"
slug: sel4-aarch64-qemu-substrate-target slug: sel4-aarch64-qemu-substrate-target
category: substrate category: substrate
last_edited: 2026-05-29 last_edited: 2026-05-29
editor: pointsav-engineering editor: pointsav-engineering
status: stable status: stable
bcsc_class: no-disclosure-implication bcsc_class: no-disclosure-implication
--- ---
The unikernel images in this platform run on the seL4 microkernel targeting the AArch64 The unikernel images in this platform run on the seL4 microkernel targeting the AArch64
instruction set architecture, with QEMU's `virt` machine model as the primary instruction set architecture, with QEMU's `virt` machine model as the primary
emulation environment for development, testing, and CI. This target was selected emulation environment for development, testing, and CI. This target was selected
through a set of architecture decisions (Group 3A and Group 3D) made in May 2026 through a set of architecture decisions (Group 3A and Group 3D) made in May 2026
and is the hardware foundation for all Phase 1C and Phase 2 work. and is the hardware foundation for all Phase 1C and Phase 2 work.
## 1. seL4 as the Microkernel Foundation ## 1. seL4 as the Microkernel Foundation
seL4 is a formally verified L4-family microkernel developed by CSIRO's Data61 and seL4 is a formally verified L4-family microkernel developed by CSIRO's Data61 and
maintained by the seL4 Foundation. Its defining property is a machine-checked proof maintained by the seL4 Foundation. Its defining property is a machine-checked proof
of functional correctness: the kernel implementation is proven to match a formal of functional correctness: the kernel implementation is proven to match a formal
specification at the Isabelle/HOL level. This proof covers the AArch64 target. specification at the Isabelle/HOL level. This proof covers the AArch64 target.
seL4 uses a capability-based access control model. Every kernel resource — memory, seL4 uses a capability-based access control model. Every kernel resource — memory,
threads, IPC endpoints, interrupt handlers — is accessible only through a capability, threads, IPC endpoints, interrupt handlers — is accessible only through a capability,
a typed unforgeable token held in a kernel-managed capability space. Sharing a a typed unforgeable token held in a kernel-managed capability space. Sharing a
resource means delegating a capability; revocation removes it. This model is the resource means delegating a capability; revocation removes it. This model is the
foundation on which the Capability Ledger Substrate is built: foundation on which the Capability Ledger Substrate is built:
the ledger extends seL4's kernel-enforced access control with a cryptographically the ledger extends seL4's kernel-enforced access control with a cryptographically
auditable record of every capability decision. auditable record of every capability decision.
The substrate does not modify the seL4 kernel. It builds on the kernel's The substrate does not modify the seL4 kernel. It builds on the kernel's
published API (libsel4) and the Microkit framework's protection-domain model. published API (libsel4) and the Microkit framework's protection-domain model.
## 2. AArch64 First ## 2. AArch64 First
The AArch64 (ARMv8-A 64-bit) architecture was selected as the primary target for The AArch64 (ARMv8-A 64-bit) architecture was selected as the primary target for
two reasons. two reasons.
First, the proof portfolio. The seL4 formal proof covers AArch64 as a first-class First, the proof portfolio. The seL4 formal proof covers AArch64 as a first-class
target, alongside x86-64 and RISC-V 64. AArch64 has the longest track record of target, alongside x86-64 and RISC-V 64. AArch64 has the longest track record of
continuous proof maintenance in the seL4 project and is used in the seL4 foundation's continuous proof maintenance in the seL4 project and is used in the seL4 foundation's
own continuous-integration pipelines. own continuous-integration pipelines.
Second, the hardware trajectory. AArch64 server processors (Ampere Altra, AWS Second, the hardware trajectory. AArch64 server processors (Ampere Altra, AWS
Graviton, Neoverse N1/V1) are available in the cloud providers relevant to the Graviton, Neoverse N1/V1) are available in the cloud providers relevant to the
deployment targets. The QEMU `virt` machine model provides a faithful AArch64 deployment targets. The QEMU `virt` machine model provides a faithful AArch64
emulation environment that maps directly to these physical targets. emulation environment that maps directly to these physical targets.
x86-64 is not excluded — seL4 supports it — but AArch64-first means that the x86-64 is not excluded — seL4 supports it — but AArch64-first means that the
toolchain investment, build infrastructure, and test matrix are calibrated to AArch64 toolchain investment, build infrastructure, and test matrix are calibrated to AArch64
from the outset. x86-64 support, if needed, inherits from the same build pipeline. from the outset. x86-64 support, if needed, inherits from the same build pipeline.
## 3. The QEMU virt Machine Model ## 3. The QEMU virt Machine Model
QEMU's `virt` machine model for AArch64 (`-machine virt`) is a synthetic platform QEMU's `virt` machine model for AArch64 (`-machine virt`) is a synthetic platform
with no fixed hardware correspondence. It is designed specifically for software with no fixed hardware correspondence. It is designed specifically for software
development and emulation. Key characteristics relevant to seL4: development and emulation. Key characteristics relevant to seL4:
**CPU:** The default target is Cortex-A53 (`-cpu cortex-a53`), an ARMv8-A **CPU:** The default target is Cortex-A53 (`-cpu cortex-a53`), an ARMv8-A
implementation with hardware virtualisation extensions. seL4 on AArch64 runs at implementation with hardware virtualisation extensions. seL4 on AArch64 runs at
Exception Level 1 (EL1) in non-virtualisation mode for the kernel, with user Exception Level 1 (EL1) in non-virtualisation mode for the kernel, with user
processes at EL0. processes at EL0.
**Interrupt controller:** GIC version 2 by default (`QEMU_GIC_VERSION=2`). **Interrupt controller:** GIC version 2 by default (`QEMU_GIC_VERSION=2`).
seL4's AArch64 port uses the ARM Generic Interrupt Controller; the QEMU virt seL4's AArch64 port uses the ARM Generic Interrupt Controller; the QEMU virt
platform provides a software GIC compatible with the seL4 driver. platform provides a software GIC compatible with the seL4 driver.
**UART:** PL011 serial controller at physical address `0x09000000`. seL4's **UART:** PL011 serial controller at physical address `0x09000000`. seL4's
`KernelPrinting` and `KernelDebugBuild` options route kernel debug output to this `KernelPrinting` and `KernelDebugBuild` options route kernel debug output to this
UART, which QEMU maps to the emulator's standard output when `-nographic` is used. UART, which QEMU maps to the emulator's standard output when `-nographic` is used.
**Device tree:** The seL4 CMake build system extracts the machine's device tree **Device tree:** The seL4 CMake build system extracts the machine's device tree
binary from QEMU at configure time, then converts it to DTS and compiles it into binary from QEMU at configure time, then converts it to DTS and compiles it into
the kernel. This is why `qemu-system-aarch64` must be present before the seL4 kernel the kernel. This is why `qemu-system-aarch64` must be present before the seL4 kernel
can be configured. can be configured.
**Physical memory:** The QEMU `virt` device tree describes physical RAM from **Physical memory:** The QEMU `virt` device tree describes physical RAM from
`0x40000000` to `0x80000000` — a 1 GiB window. QEMU must be launched with at least `0x40000000` to `0x80000000` — a 1 GiB window. QEMU must be launched with at least
`-m 1G`; booting with less allocates physical memory that does not cover the full `-m 1G`; booting with less allocates physical memory that does not cover the full
window described to the kernel, causing the elfloader to fail when placing images window described to the kernel, causing the elfloader to fail when placing images
within the expected range. within the expected range.
## 4. Kernel Build Configuration ## 4. Kernel Build Configuration
The seL4 kernel is built from source at `vendor-sel4-kernel/src/` using CMake with The seL4 kernel is built from source at `vendor-sel4-kernel/src/` using CMake with
a GCC cross-compile toolchain. The critical configuration options for the QEMU a GCC cross-compile toolchain. The critical configuration options for the QEMU
AArch64 target are: AArch64 target are:
``` ```
-DCMAKE_C_COMPILER=aarch64-linux-gnu-gcc -DCMAKE_C_COMPILER=aarch64-linux-gnu-gcc
-DCMAKE_ASM_COMPILER=aarch64-linux-gnu-gcc -DCMAKE_ASM_COMPILER=aarch64-linux-gnu-gcc
-DCROSS_COMPILER_PREFIX=aarch64-linux-gnu- -DCROSS_COMPILER_PREFIX=aarch64-linux-gnu-
-DKernelPlatform=qemu-arm-virt -DKernelPlatform=qemu-arm-virt
-DKernelArch=arm -DKernelArch=arm
-DKernelSel4Arch=aarch64 -DKernelSel4Arch=aarch64
-DKernelVerificationBuild=OFF -DKernelVerificationBuild=OFF
-DKernelPrinting=ON -DKernelPrinting=ON
-DKernelDebugBuild=ON -DKernelDebugBuild=ON
``` ```
`KernelVerificationBuild=OFF` is required for `KernelPrinting=ON` to take effect. `KernelVerificationBuild=OFF` is required for `KernelPrinting=ON` to take effect.
When `KernelVerificationBuild=ON`, the CMake configuration silently disables When `KernelVerificationBuild=ON`, the CMake configuration silently disables
`CONFIG_PRINTING` — the CMake cache records `KernelPrinting_DISABLED:INTERNAL=TRUE` `CONFIG_PRINTING` — the CMake cache records `KernelPrinting_DISABLED:INTERNAL=TRUE`
without warning, and the kernel produces no serial output. without warning, and the kernel produces no serial output.
`KernelPrinting=ON` enables the kernel's serial output via the PL011 UART. `KernelPrinting=ON` enables the kernel's serial output via the PL011 UART.
`KernelDebugBuild=ON` enables debug assertions and additional diagnostic output. `KernelDebugBuild=ON` enables debug assertions and additional diagnostic output.
Both are appropriate for development and testing; a production image would use Both are appropriate for development and testing; a production image would use
`CMAKE_BUILD_TYPE=Release` without these options. `CMAKE_BUILD_TYPE=Release` without these options.
The build produces `kernel.elf`, a statically linked AArch64 ELF executable with The build produces `kernel.elf`, a statically linked AArch64 ELF executable with
entry point `0xffffff8040000000` — the kernel's intended virtual address once the entry point `0xffffff8040000000` — the kernel's intended virtual address once the
AArch64 MMU is configured. As of Phase 1C.b (2026-05-27), this build succeeds from AArch64 MMU is configured. As of Phase 1C.b (2026-05-27), this build succeeds from
the seL4 v15.0.0-dev source tree with `aarch64-linux-gnu-gcc` v13.3.0 on Ubuntu 24.04. the seL4 v15.0.0-dev source tree with `aarch64-linux-gnu-gcc` v13.3.0 on Ubuntu 24.04.
## 5. The Elfloader and the Boot Chain ## 5. The Elfloader and the Boot Chain
The seL4 kernel ELF for AArch64 has a link-time entry point at virtual address The seL4 kernel ELF for AArch64 has a link-time entry point at virtual address
`0xffffff8040000000`. This is the kernel's intended virtual address once the AArch64 `0xffffff8040000000`. This is the kernel's intended virtual address once the AArch64
MMU is configured and the kernel's own page tables are in place. QEMU cannot load the MMU is configured and the kernel's own page tables are in place. QEMU cannot load the
kernel ELF directly — it would attempt to place it at that virtual address in physical kernel ELF directly — it would attempt to place it at that virtual address in physical
memory, which does not exist on the `virt` machine. memory, which does not exist on the `virt` machine.
The standard seL4 boot flow uses the **elfloader**, a small bootstrap program from The standard seL4 boot flow uses the **elfloader**, a small bootstrap program from
the `seL4_tools` repository (vendored at `vendor-sel4-tools/elfloader-tool/`). The the `seL4_tools` repository (vendored at `vendor-sel4-tools/elfloader-tool/`). The
elfloader: elfloader:
1. Runs from physical address `0x40400000`, where QEMU can load it directly. 1. Runs from physical address `0x40400000`, where QEMU can load it directly.
2. Unpacks the seL4 kernel ELF from a CPIO archive embedded in the loader image. 2. Unpacks the seL4 kernel ELF from a CPIO archive embedded in the loader image.
3. Configures the AArch64 MMU page tables to map the kernel's virtual address space. 3. Configures the AArch64 MMU page tables to map the kernel's virtual address space.
4. Unpacks the initial user-level thread (rootserver) from the same CPIO archive. 4. Unpacks the initial user-level thread (rootserver) from the same CPIO archive.
5. Jumps to the kernel entry point, now reachable through the MMU mapping. 5. Jumps to the kernel entry point, now reachable through the MMU mapping.
The combined image — elfloader binary with the kernel, device tree, and rootserver The combined image — elfloader binary with the kernel, device tree, and rootserver
embedded as a CPIO archive — is what QEMU actually boots. embedded as a CPIO archive — is what QEMU actually boots.
As of Phase 1C.d (moonshot-toolkit v0.3.0), this image is assembled automatically As of Phase 1C.d (moonshot-toolkit v0.3.0), this image is assembled automatically
by the `moonshot-toolkit build` command. The AssembleImage step compiles the elfloader by the `moonshot-toolkit build` command. The AssembleImage step compiles the elfloader
sources, generates the CPIO archive using a pure Rust writer, and links the combined sources, generates the CPIO archive using a pure Rust writer, and links the combined
binary. No Python, CMake, or shell scripts are involved in the image assembly path. binary. No Python, CMake, or shell scripts are involved in the image assembly path.
## 6. Phase 1C Boot Chain — Verified ## 6. Phase 1C Boot Chain — Verified
Phase 1C is complete. The full AArch64 boot chain from source to QEMU output has been Phase 1C is complete. The full AArch64 boot chain from source to QEMU output has been
demonstrated on the workspace VM. demonstrated on the workspace VM.
**Phase 1C.b** (completed 2026-05-27): the seL4 kernel for QEMU AArch64 was built **Phase 1C.b** (completed 2026-05-27): the seL4 kernel for QEMU AArch64 was built
from source. `vendor-sel4-kernel/build/aarch64-qemu/kernel.elf` is a valid AArch64 from source. `vendor-sel4-kernel/build/aarch64-qemu/kernel.elf` is a valid AArch64
static ELF, entry point `0xffffff8040000000`. static ELF, entry point `0xffffff8040000000`.
**Phase 1C.c** (completed 2026-05-28): full QEMU boot confirmed. A manually assembled **Phase 1C.c** (completed 2026-05-28): full QEMU boot confirmed. A manually assembled
elfloader image was loaded by QEMU, producing kernel output through the PL011 UART elfloader image was loaded by QEMU, producing kernel output through the PL011 UART
and handing off to a minimal rootserver. and handing off to a minimal rootserver.
**Phase 1C.d** (completed 2026-05-29): moonshot-toolkit v0.3.0 automates the full **Phase 1C.d** (completed 2026-05-29): moonshot-toolkit v0.3.0 automates the full
pipeline. The command: pipeline. The command:
``` ```
cargo run -p moonshot-toolkit -- build moonshot-toolkit/examples/hello-world.toml cargo run -p moonshot-toolkit -- build moonshot-toolkit/examples/hello-world.toml
``` ```
produces `build/system-image.bin` with entry point `0x40400000`. Booting with: produces `build/system-image.bin` with entry point `0x40400000`. Booting with:
``` ```
qemu-system-aarch64 -machine virt,secure=off -cpu cortex-a53 \ qemu-system-aarch64 -machine virt,secure=off -cpu cortex-a53 \
-m 1G -nographic -kernel build/system-image.bin -m 1G -nographic -kernel build/system-image.bin
``` ```
produces: produces:
``` ```
ELF-loader started on CPU: ARM Ltd. Cortex-A53 r0p4 ELF-loader started on CPU: ARM Ltd. Cortex-A53 r0p4
paddr=[40400000..40423fff] paddr=[40400000..40423fff]
Bootstrapping kernel Bootstrapping kernel
… …
Booting all finished, dropped to user space Booting all finished, dropped to user space
``` ```
## See Also ## See Also
- [[moonshot-toolkit-build-orchestrator]] — the Rust build orchestrator that - [[moonshot-toolkit-build-orchestrator]] — the Rust build orchestrator that
cross-compiles protection domains and assembles this target's boot image cross-compiles protection domains and assembles this target's boot image
- [[capability-ledger-substrate]] — what the unikernel images enforce at runtime - [[capability-ledger-substrate]] — what the unikernel images enforce at runtime