Diff: substrate/moonshot-toolkit-build-orchestrator.es
From 06b1da5 to 06b1da5
+0 / −0 lines
| Before | After |
|---|---|
| --- | --- |
| schema: foundry-doc-v1 | schema: foundry-doc-v1 |
| title: "The moonshot-toolkit Build Orchestrator" | title: "The moonshot-toolkit Build Orchestrator" |
| slug: moonshot-toolkit-build-orchestrator | slug: moonshot-toolkit-build-orchestrator |
| 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 |
| --- | --- |
| moonshot-toolkit is a Rust-only build orchestrator for seL4 unikernel images, | moonshot-toolkit is a Rust-only build orchestrator for seL4 unikernel images, |
| replacing the Python and CMake toolchain provided by the seL4 Microkit framework. It | replacing the Python and CMake toolchain provided by the seL4 Microkit framework. It |
| reads a TOML system specification, derives a deterministic content-addressed build | reads a TOML system specification, derives a deterministic content-addressed build |
| manifest, and orchestrates the cross-compilation and image assembly pipeline through to | manifest, and orchestrates the cross-compilation and image assembly pipeline through to |
| a bootable elfloader binary for the AArch64 target. | a bootable elfloader binary for the AArch64 target. |
| ## 1. Why Rust-Only | ## 1. Why Rust-Only |
| The seL4 Microkit framework ships a Python image-assembly script and a CMake build | The seL4 Microkit framework ships a Python image-assembly script and a CMake build |
| system. These tools are adequate for general embedded development but present three | system. These tools are adequate for general embedded development but present three |
| problems for a reproducible-build discipline. | problems for a reproducible-build discipline. |
| First, determinism. Python dictionary ordering is implementation-defined; CMake | First, determinism. Python dictionary ordering is implementation-defined; CMake |
| dependency discovery varies across versions. A Rust binary built from a fixed source | dependency discovery varies across versions. A Rust binary built from a fixed source |
| revision with vendored dependencies produces bit-identical plan bytes across machines | revision with vendored dependencies produces bit-identical plan bytes across machines |
| and over time. | and over time. |
| Second, auditability. A single Rust binary is an auditable end-to-end artefact. | Second, auditability. A single Rust binary is an auditable end-to-end artefact. |
| Python scripts, CMake modules, Makefiles, and shell wrappers compose a multi-language | Python scripts, CMake modules, Makefiles, and shell wrappers compose a multi-language |
| audit surface that is difficult to reason about formally. | audit surface that is difficult to reason about formally. |
| Third, network isolation. The Reproducible-Verification-On-Customer-Metal | Third, network isolation. The Reproducible-Verification-On-Customer-Metal |
| convention requires that build steps run without network access. Python's `pip install` | convention requires that build steps run without network access. Python's `pip install` |
| and CMake's `find_package` are live network surfaces. A Rust binary with vendored | and CMake's `find_package` are live network surfaces. A Rust binary with vendored |
| dependencies eliminates them. | dependencies eliminates them. |
| ## 2. SystemSpec — The Input | ## 2. SystemSpec — The Input |
| A system specification is a TOML file that describes a seL4 Microkit system. It is | A system specification is a TOML file that describes a seL4 Microkit system. It is |
| the Rust-native equivalent of Microkit 2.2.0's system-description XML schema. | the Rust-native equivalent of Microkit 2.2.0's system-description XML schema. |
| The specification declares four collections: | The specification declares four collections: |
| **Protection domains** are isolated, single-threaded software components scheduled by | **Protection domains** are isolated, single-threaded software components scheduled by |
| the seL4 kernel. Each domain has a name, a path to its source binary, a scheduling | the seL4 kernel. Each domain has a name, a path to its source binary, a scheduling |
| priority (0 is highest, matching seL4 and Microkit conventions), and a stack size in | priority (0 is highest, matching seL4 and Microkit conventions), and a stack size in |
| bytes (defaulting to 4 KiB per Microkit). The system may contain at most 63 protection | bytes (defaulting to 4 KiB per Microkit). The system may contain at most 63 protection |
| domains, the hard limit imposed by the Microkit framework. | domains, the hard limit imposed by the Microkit framework. |
| **Channels** are point-to-point communication links between protection domains, using | **Channels** are point-to-point communication links between protection domains, using |
| seL4's Protected Procedure Call or notification mechanisms. Each protection domain | seL4's Protected Procedure Call or notification mechanisms. Each protection domain |
| may have at most 63 channels. | may have at most 63 channels. |
| **Memory regions** declare physical memory mappings with caching and permission | **Memory regions** declare physical memory mappings with caching and permission |
| attributes and an optional prefill from a binary blob. Overlapping regions are | attributes and an optional prefill from a binary blob. Overlapping regions are |
| rejected at parse time. | rejected at parse time. |
| **IRQ delivery** entries bind hardware interrupt lines to specific protection domains. | **IRQ delivery** entries bind hardware interrupt lines to specific protection domains. |
| Validation rules are enforced during parsing: no duplicate domain names, all channel | Validation rules are enforced during parsing: no duplicate domain names, all channel |
| endpoints and IRQ targets must reference declared domains, and memory regions must | endpoints and IRQ targets must reference declared domains, and memory regions must |
| not overlap. | not overlap. |
| A minimal hello-world specification looks like: | A minimal hello-world specification looks like: |
| ```toml | ```toml |
| [[protection_domains]] | [[protection_domains]] |
| name = "hello" | name = "hello" |
| binary = "moonshot-toolkit/examples/hello.c" | binary = "moonshot-toolkit/examples/hello.c" |
| priority = 100 | priority = 100 |
| stack_bytes = 65536 | stack_bytes = 65536 |
| ``` | ``` |
| ## 3. BuildPlan — The Manifest | ## 3. BuildPlan — The Manifest |
| Given a parsed SystemSpec, moonshot-toolkit generates a BuildPlan: a deterministic, | Given a parsed SystemSpec, moonshot-toolkit generates a BuildPlan: a deterministic, |
| content-addressed build manifest. | content-addressed build manifest. |
| The plan contains three fields. The `spec_hash` is the SHA-256 digest of the canonical | The plan contains three fields. The `spec_hash` is the SHA-256 digest of the canonical |
| TOML rendering of the SystemSpec — it identifies the input. The `steps` field is an | TOML rendering of the SystemSpec — it identifies the input. The `steps` field is an |
| ordered list of build steps: one CompilePd step per protection domain followed by a | ordered list of build steps: one CompilePd step per protection domain followed by a |
| single AssembleImage step. The `plan_hash` is the SHA-256 digest of the canonical | single AssembleImage step. The `plan_hash` is the SHA-256 digest of the canonical |
| JSON rendering of `(spec_hash, steps)` — it is the value the customer-apex cosignature | JSON rendering of `(spec_hash, steps)` — it is the value the customer-apex cosignature |
| commits to. | commits to. |
| The determinism guarantee is strict: the same SystemSpec always produces the same | The determinism guarantee is strict: the same SystemSpec always produces the same |
| `plan_hash`. This property is covered by tests and is foundational to the | `plan_hash`. This property is covered by tests and is foundational to the |
| Reproducible-Verification-On-Customer-Metal convention: a customer can verify that a | Reproducible-Verification-On-Customer-Metal convention: a customer can verify that a |
| delivered binary corresponds to a known specification by recomputing the plan_hash and | delivered binary corresponds to a known specification by recomputing the plan_hash and |
| comparing it against a cosigned value. | comparing it against a cosigned value. |
| ## 4. Build Commands | ## 4. Build Commands |
| A BuildPlan contains two kinds of steps. | A BuildPlan contains two kinds of steps. |
| **CompilePd** cross-compiles a protection domain's source file to a bare-metal AArch64 | **CompilePd** cross-compiles a protection domain's source file to a bare-metal AArch64 |
| ELF binary. The invocation uses the `aarch64-linux-gnu-gcc` cross-compiler with flags | ELF binary. The invocation uses the `aarch64-linux-gnu-gcc` cross-compiler with flags |
| appropriate for seL4 Microkit protection domains: | appropriate for seL4 Microkit protection domains: |
| - `-nostdlib -nostartfiles`: no C standard library or startup files; the protection | - `-nostdlib -nostartfiles`: no C standard library or startup files; the protection |
| domain provides its own `_start` entry point. | domain provides its own `_start` entry point. |
| - `-ffreestanding`: no hosted-environment assumptions; no implicit includes. | - `-ffreestanding`: no hosted-environment assumptions; no implicit includes. |
| - `-static -no-pie`: Microkit loads PD binaries at fixed virtual addresses; dynamic | - `-static -no-pie`: Microkit loads PD binaries at fixed virtual addresses; dynamic |
| linking is not available. | linking is not available. |
| - `-march=armv8-a`: target AArch64 ISA. | - `-march=armv8-a`: target AArch64 ISA. |
| - `-mgeneral-regs-only`: exclude FPU and SIMD registers; the seL4 kernel does not | - `-mgeneral-regs-only`: exclude FPU and SIMD registers; the seL4 kernel does not |
| save FPU state by default. | save FPU state by default. |
| The output is a statically linked ELF executable targeting the AArch64 architecture. | The output is a statically linked ELF executable targeting the AArch64 architecture. |
| **AssembleImage** produces the bootable system image. It executes in pure Rust without | **AssembleImage** produces the bootable system image. It executes in pure Rust without |
| invoking Python, CMake, or shell scripts, in five stages: | invoking Python, CMake, or shell scripts, in five stages: |
| 1. **CPIO archive**: the protection-domain binaries, the seL4 kernel ELF, and the | 1. **CPIO archive**: the protection-domain binaries, the seL4 kernel ELF, and the |
| kernel device tree binary are packed into a CPIO "newc" archive using a Rust-native | kernel device tree binary are packed into a CPIO "newc" archive using a Rust-native |
| writer (`src/cpio.rs`). The writer implements the exact 110-byte ASCII header format | writer (`src/cpio.rs`). The writer implements the exact 110-byte ASCII header format |
| and 4-byte-aligned padding that the seL4 elfloader's CPIO parser requires. | and 4-byte-aligned padding that the seL4 elfloader's CPIO parser requires. |
| 2. **Archive embedding**: the CPIO archive is embedded into an assembly stub | 2. **Archive embedding**: the CPIO archive is embedded into an assembly stub |
| (`archive.S`) using `.incbin`. This file is compiled as one object in the final link. | (`archive.S`) using `.incbin`. This file is compiled as one object in the final link. |
| 3. **Elfloader compilation**: the 44 C and ASM source files of the seL4 elfloader | 3. **Elfloader compilation**: the 44 C and ASM source files of the seL4 elfloader |
| (from `vendor-sel4-tools/elfloader-tool/`) are compiled with AArch64 bare-metal | (from `vendor-sel4-tools/elfloader-tool/`) are compiled with AArch64 bare-metal |
| flags, together with the seL4 libcpio helper library. All include paths — elfloader | flags, together with the seL4 libcpio helper library. All include paths — elfloader |
| headers, CMake-generated configuration headers, kernel autoconf — are resolved from | headers, CMake-generated configuration headers, kernel autoconf — are resolved from |
| the vendor trees present in the repository. | the vendor trees present in the repository. |
| 4. **Link**: all objects are linked with `-nostdlib -static -lgcc` using a preprocessed | 4. **Link**: all objects are linked with `-nostdlib -static -lgcc` using a preprocessed |
| version of the elfloader's linker script. The result is a bare-metal AArch64 ELF | version of the elfloader's linker script. The result is a bare-metal AArch64 ELF |
| with entry point `0x40400000`. | with entry point `0x40400000`. |
| 5. **Output**: the linked ELF is copied to the specified output path (default: | 5. **Output**: the linked ELF is copied to the specified output path (default: |
| `build/system-image.bin`). | `build/system-image.bin`). |
| ## 5. Reproducibility and Cosignature | ## 5. Reproducibility and Cosignature |
| The plan_hash ties together the input specification and the full ordered build procedure. | The plan_hash ties together the input specification and the full ordered build procedure. |
| A customer receiving a binary artefact can verify its provenance by: | A customer receiving a binary artefact can verify its provenance by: |
| 1. Reconstructing the SystemSpec from the shipped TOML. | 1. Reconstructing the SystemSpec from the shipped TOML. |
| 2. Running `moonshot-toolkit plan` to derive the BuildPlan. | 2. Running `moonshot-toolkit plan` to derive the BuildPlan. |
| 3. Comparing the computed plan_hash against the value in the vendor's cosigned manifest. | 3. Comparing the computed plan_hash against the value in the vendor's cosigned manifest. |
| 4. Optionally rerunning `moonshot-toolkit build` on their own infrastructure to verify | 4. Optionally rerunning `moonshot-toolkit build` on their own infrastructure to verify |
| the binary byte-for-byte. | the binary byte-for-byte. |
| This chain satisfies the Capability Ledger Substrate property: cryptographically auditable | This chain satisfies the Capability Ledger Substrate property: cryptographically auditable |
| access-control decisions anchored to logs the customer controls. The plan_hash is the | access-control decisions anchored to logs the customer controls. The plan_hash is the |
| point at which the cosignature (Sigstore Cosign with customer-apex key) attaches. | point at which the cosignature (Sigstore Cosign with customer-apex key) attaches. |
| ## 6. Phase 1C Status | ## 6. Phase 1C Status |
| moonshot-toolkit v0.3.0, released 2026-05-29, completes the Phase 1C milestone: | moonshot-toolkit v0.3.0, released 2026-05-29, completes the Phase 1C milestone: |
| - **Phase 1C.a** (v0.2.0, 2026-05-27): CompilePd invokes the real AArch64 | - **Phase 1C.a** (v0.2.0, 2026-05-27): CompilePd invokes the real AArch64 |
| cross-compiler and produces a verified bare-metal ELF. Confirmed: `build/hello.elf`, | cross-compiler and produces a verified bare-metal ELF. Confirmed: `build/hello.elf`, |
| entry point `0x40010c`. | entry point `0x40010c`. |
| - **Phase 1C.b** (2026-05-27): seL4 AArch64 kernel built from source with | - **Phase 1C.b** (2026-05-27): seL4 AArch64 kernel built from source with |
| `KernelPlatform=qemu-arm-virt`. The `kernel.elf` at `vendor-sel4-kernel/build/aarch64-qemu/` | `KernelPlatform=qemu-arm-virt`. The `kernel.elf` at `vendor-sel4-kernel/build/aarch64-qemu/` |
| is a valid AArch64 ELF, entry point `0xffffff8040000000`. | is a valid AArch64 ELF, entry point `0xffffff8040000000`. |
| - **Phase 1C.c** (2026-05-28): full QEMU boot confirmed. elfloader → seL4 kernel → | - **Phase 1C.c** (2026-05-28): full QEMU boot confirmed. elfloader → seL4 kernel → |
| rootserver chain produces output: "Booting all finished, dropped to user space". | rootserver chain produces output: "Booting all finished, dropped to user space". |
| - **Phase 1C.d** (v0.3.0, 2026-05-29): AssembleImage fully implemented in Rust. | - **Phase 1C.d** (v0.3.0, 2026-05-29): AssembleImage fully implemented in Rust. |
| `moonshot-toolkit build moonshot-toolkit/examples/hello-world.toml` produces | `moonshot-toolkit build moonshot-toolkit/examples/hello-world.toml` produces |
| `build/system-image.bin`, entry point `0x40400000`. QEMU boots the image using | `build/system-image.bin`, entry point `0x40400000`. QEMU boots the image using |
| `-m 1G -kernel build/system-image.bin`. | `-m 1G -kernel build/system-image.bin`. |
| The complete build pipeline — from TOML specification to a booting seL4 system — now | The complete build pipeline — from TOML specification to a booting seL4 system — now |
| runs in a single `cargo run` invocation with no Python, CMake, or shell in the | runs in a single `cargo run` invocation with no Python, CMake, or shell in the |
| critical path. | critical path. |
| ## See Also | ## See Also |
| - [[sel4-aarch64-qemu-substrate-target]] — the seL4 kernel target that | - [[sel4-aarch64-qemu-substrate-target]] — the seL4 kernel target that |
| moonshot-toolkit's images run on | moonshot-toolkit's images run on |
| - [[capability-ledger-substrate]] — what the built images enforce at runtime | - [[capability-ledger-substrate]] — what the built images enforce at runtime |