# The seL4 configuration of loader.img, written by tools/sel4-config.
# A verification statement about this image must match this record.
image: loader.img
image-sha256: e7296ab088d7090551ed484bce1ff6a544164a4ce20189ce2c5b7c4e7cfbd33e
system: ui-interactive
board: qemu_virt_aarch64
configuration: debug
sdk: Microkit 2.3.1
sdk-archive: microkit-sdk-2.3.1-linux-aarch64.tar.gz
sdk-sha256: 979553f288e8e2c099dae8fbec86cbe2cfda2ca006ee36de8234649d6d23bbee (pinned in tools/container/Containerfile; checked when the dev image was built)
kernel: board/qemu_virt_aarch64/debug/elf/sel4.elf in the SDK
kernel-sha256: 646a412595a975fb1f6fcba812f72916673efe26a6fc758f4cb509906cc1ff5b
position: tools/sel4-verification.toml, checked 2026-10-03 for this SDK (seL4 16.0.0)
status: development build: a debug kernel, with printing and debug interfaces, outside seL4's proofs
status: outside seL4's completed proofs: a mixed-criticality (MCS) kernel, whose AArch64 proofs are in progress
status: outside seL4's proofs: a platform that is not on seL4's AArch64 verified list
status: not seL4's AArch64 verified configuration: differs in VERIFICATION_BUILD, PRINTING, MAX_NUM_BOOTINFO_UNTYPED_CAPS

# Kernel options that decide proof coverage, from board/qemu_virt_aarch64/debug/include/kernel/gen_config.json:
# option                         this kernel    seL4's AArch64 verified configuration
PLAT                             qemu-arm-virt  one of: bcm2712  DIFFERS
SEL4_ARCH                        aarch64        aarch64
ARM_HYPERVISOR_SUPPORT           true           true
VERIFICATION_BUILD               false          true  DIFFERS
DEBUG_BUILD                      true           false  DIFFERS
MAX_NUM_NODES                    1              1
ENABLE_SMP_SUPPORT               false          false
KERNEL_MCS                       true           false  DIFFERS
KERNEL_OPT_LEVEL                 -O2            -O2
RETYPE_FAN_OUT_LIMIT             256            256
KERNEL_BENCHMARK                 none           none
DANGEROUS_CODE_INJECTION         false          false
FASTPATH                         true           true
PRINTING                         true           false  DIFFERS
NUM_DOMAINS                      16             16
MAX_NUM_BOOTINFO_UNTYPED_CAPS    230            50  DIFFERS
ARM_SMMU                         false          false
ALLOW_SMC_CALLS                  true           true

# Even a kernel that matches every option above is covered by seL4's proofs only as far as they go:
# not its boot code, the System MMU, the debug and printing interfaces, or anything outside the
# kernel - Microkit's tools, its monitor and the protection domains.