Attribution
Open-source components
The Parsimoni Platform uses these open-source components:
- Solo5 provides the
hvtandspttenders for unikernel workloads. - MirageOS provides the OCaml unikernel framework.
- Unikraft provides a POSIX-compatible unikernel framework for C, C++, and Rust applications.
- runc provides the OCI container runtime. The Platform uses it for container workloads and build-step sandboxes.
- Firecracker provides the virtual machine monitor for the
firecrackerbackend and for the machine the runner raises for a tenant's containers. - Kata Containers defines the agent protocol the runner speaks to the container agent inside a tenant's machine.
- QEMU provides the x86-64 system emulator for the
qemubackend, and the VM launcher on Linux hosts. - Linux provides the node kernel, packaged as the
uniboot-kernelimage.
Verification scope
A proof about an upstream component covers the code and the properties that
proof names. It says nothing about the rest of that component, or about the
Platform around it. The one proof the Space CLI links today is Vale's: the
x86-64 AES-GCM assembly is verified correct and constant-time in F*. It covers
that kernel alone, and on AArch64 there is no verified kernel to link, because
Vale has no AArch64 backend. space version reports which AES-GCM kernel a
binary links, as space version describes. The seL4 proof
covers the seL4 kernel alone, as substrates states.
Design lineage
These systems influenced the Platform architecture without contributing code to it:
- LinuxKit influenced the minimal-init and OCI image composition model. Space CLI uses an OCaml image assembler for this model.
- OBuilder influenced the content-addressed build steps and their runc sandboxes.
- Albatross influenced the unikernel supervision model used by the runner and its agents.
- Dagger influenced the common service model for build steps and runtime services. It also influenced the two-layer build cache.
Licenses
Documentation under src/content/docs/ is licensed under the Creative
Commons Attribution-NoDerivatives 4.0 International License.
You may share unchanged copies with attribution to Parsimoni. The license does
not permit distribution of modified copies.
The Astro configuration, components, styles, scripts, and other site source are licensed under the MIT License. Third-party components retain their own licenses.
