Microkit on QEMU: The Basic Toolchain

Before putting a larger Microkit system together, I start with one small checkpoint: build a program, package it with the SDK, and see its output in QEMU. That gives me a working baseline before adding more components.

This note covers two x86-64 hosts: an Intel Mac and Ubuntu 24.04 Linux. Both build the same AArch64 system for QEMU. Select macOS or Ubuntu above a code window to show the commands for that host. The other command tabs switch with it.

Use the matching host archive from the official release if you are working on Apple Silicon or an AArch64 Linux host.

The Starting Point

These are the two environments used for the build and boot checks:

The compiler produces the AArch64 program. Microkit combines that program and a system description with its bundled runtime and kernel. QEMU then boots the resulting image. The Microkit 2.4.0 release notes identify the bundled kernel version.

Select the Host Tools

On macOS, start with Apple's Command Line Tools and Homebrew. On Ubuntu, use the distribution's AArch64 cross compiler, binutils, Make, and QEMU packages. Check that uname -m reports x86_64 for the SDK downloads used here:

uname -m
xcode-select -p
brew --version
brew install make aarch64-elf-gcc aarch64-elf-binutils qemu
export PATH="$(brew --prefix make)/libexec/gnubin:$PATH"
hash -r
make --version
aarch64-elf-gcc --version
aarch64-elf-ld --version
qemu-system-aarch64 --version

uname -m
sudo apt-get update
sudo apt-get install --yes --no-install-recommends \
  make gcc-aarch64-linux-gnu binutils-aarch64-linux-gnu \
  qemu-system-arm curl ca-certificates
make --version
aarch64-linux-gnu-gcc --version
aarch64-linux-gnu-ld --version
qemu-system-aarch64 --version

For a new Mac installation, follow Apple's developer tools instructions and Homebrew's installation guide first. Homebrew normally exposes GNU Make as gmake; the gnubin path above makes it available as make for this shell. My existing Mac installation already exposes GNU Make 4.3 as make.

Package managers resolve their current packages, which can differ from a recorded environment. The Mac checkpoint used the listed versions on an existing installation rather than a fresh installation of today's formulae. Ubuntu's package names follow the upstream Microkit setup instructions.

Get the Microkit SDK

Use a versioned SDK rather than mixing a kernel build with unrelated headers and tools. Each tab downloads its host's archive, checks the corresponding SHA-256 digest, and extracts it into a new directory:

(
  set -eu
  mkdir -p "$HOME/dev/toolchains"
  cd "$HOME/dev/toolchains"

  archive=microkit-sdk-2.4.0-macos-x86-64.tar.gz
  curl --fail --location --output "$archive" \
    "https://github.com/seL4/microkit/releases/download/2.4.0/$archive"

  printf '%s  %s\n' \
    1dccd998a2cd01112fa650590810afd328a40d9ff29e0d0baf193910f16453f1 \
    "$archive" | shasum -a 256 -c -

  test ! -e microkit-sdk-2.4.0
  tar -xzf "$archive"
)

export MICROKIT_SDK="$HOME/dev/toolchains/microkit-sdk-2.4.0"

(
  set -eu
  mkdir -p "$HOME/dev/toolchains"
  cd "$HOME/dev/toolchains"

  archive=microkit-sdk-2.4.0-linux-x86-64.tar.gz
  curl --fail --location --output "$archive" \
    "https://github.com/seL4/microkit/releases/download/2.4.0/$archive"

  printf '%s  %s\n' \
    10bc305713965a01e52b6c7567cea4952b0cc4dde4befa2e6e72b8dce2715f6b \
    "$archive" | sha256sum -c -

  test ! -e microkit-sdk-2.4.0
  tar -xzf "$archive"
)

export MICROKIT_SDK="$HOME/dev/toolchains/microkit-sdk-2.4.0"

The checksums match the official release asset metadata. The extraction check stops the sequence from overwriting an existing SDK directory. If the SDK is already installed, set MICROKIT_SDK to that installation instead.

Confirm the version and board files:

cat "$MICROKIT_SDK/VERSION"
test -d "$MICROKIT_SDK/board/qemu_virt_aarch64/debug"
"$MICROKIT_SDK/bin/microkit" --help

VERSION should contain 2.4.0. MICROKIT_SDK must point to the directory containing VERSION, bin, board, and example directly.

Build the Hello Example

The SDK includes a small hello example. Copy it into a fresh workspace so the SDK remains a clean reference:

mkdir -p "$HOME/dev"
microkit_workdir="$(mktemp -d "$HOME/dev/microkit-qemu.XXXXXX")"
cp -R "$MICROKIT_SDK/example/hello" "$microkit_workdir/hello"
cd "$microkit_workdir/hello"
mkdir build

Keep this shell open for the remaining commands. Build with the AArch64 tools selected earlier:

make \
  MICROKIT_SDK="$MICROKIT_SDK" \
  MICROKIT_BOARD=qemu_virt_aarch64 \
  MICROKIT_CONFIG=debug \
  BUILD_DIR="$PWD/build" \
  CC=aarch64-elf-gcc \
  LD=aarch64-elf-ld \
  AS=aarch64-elf-as

make \
  MICROKIT_SDK="$MICROKIT_SDK" \
  MICROKIT_BOARD=qemu_virt_aarch64 \
  MICROKIT_CONFIG=debug \
  BUILD_DIR="$PWD/build" \
  CC=aarch64-linux-gnu-gcc \
  LD=aarch64-linux-gnu-ld \
  AS=aarch64-linux-gnu-as

The compiler overrides matter: the SDK's hello Makefile defaults to aarch64-none-elf for this target. The Mac path uses aarch64-elf; Ubuntu uses aarch64-linux-gnu. Command-line Make variables select the matching tools without editing the example.

The build produces:

Boot It in QEMU

Run this from the hello workspace:

qemu-system-aarch64 \
  -machine virt,virtualization=on \
  -cpu cortex-a53 \
  -smp 1 \
  -m 2G \
  -nographic \
  -serial mon:stdio \
  -nic none \
  -device loader,file=build/loader.img,addr=0x70000000,cpu-num=0

qemu-system-aarch64 \
  -object memory-backend-ram,id=guestmem,size=2G,reserve=off \
  -machine virt,virtualization=on,memory-backend=guestmem \
  -cpu cortex-a53 \
  -smp 1 \
  -m 2G \
  -nographic \
  -serial mon:stdio \
  -nic none \
  -device loader,file=build/loader.img,addr=0x70000000,cpu-num=0

The machine, CPU, memory size, and loader address follow the versioned manual's QEMU AArch64 board instructions. This run uses one virtual CPU and no network interface.

The Linux command skips upfront host memory reservation with reserve=off, while preserving the board's 2 GiB guest memory. This was needed inside the small Linux test VM. QEMU documents the memory backend options.

After the kernel and Microkit startup output, the example prints:

hello, world

That is output from the protection domain's initialization function. It is not a Linux shell prompt. The system stays running after the message; press Ctrl+A, release the keys, then press X to leave QEMU.

Check the Result

For this note, I built fresh copies of the SDK's unmodified hello example on the native Intel Mac and in an Ubuntu 24.04 container. Both builds exited successfully, both QEMU runs printed hello, world, and both emulators exited normally after the Ctrl+A, X sequence. The Linux boot used the memory-backend option shown in its tab.

That is the checkpoint: the compiler, SDK, system description, loader image, and emulator work together. Adding application components and exploring their interfaces can start from this baseline.

A Few Setup Snags

• aarch64-none-elf-gcc not found: include the CC, LD, and AS overrides from the tab matching your host.
• MICROKIT_SDK must be specified: export the SDK path again in the shell running Make. An exported variable from another terminal does not carry over.
• Missing build directory: create it before invoking the upstream Makefile; its object rules expect the directory to exist.
• QEMU starts but no hello message appears: check the board name, the image path, and the complete console output. Keep the CPU, memory size, and loader address paired with this SDK board configuration.

References

• Microkit 2.4.0 release and SDK downloads
• Microkit 2.4.0 user manual
• Upstream hello example and its BSD-2-Clause attribution
• Homebrew GNU Make, AArch64 GCC, binutils, and QEMU