linux: run Go and musl threads in a guest, let them wait as on Linux, and end the guest whole

.github/workflows/ci-iso.yml

@@ -88,7 +88,7 @@ jobs:
 
       # Build the flashable image. This drives, in order: build and sign every
       # capsule, enroll the whole set under one STARK policy root and emit each
-      # NZKSTRK1 trailer, build and dual-sign the kernel, enroll the kernel and
+      # NZKSTRK2 trailer, build and dual-sign the kernel, enroll the kernel and
       # embed its STARK self-attestation trailer, build the bootloader with the
       # stark-kernel-attest check and the enrolled kernel root, and package the
       # GPT/FAT32 image.

.github/workflows/verify.yml

@@ -115,6 +115,18 @@ jobs:
         run: python3 scripts/check_service_caps.py
       - name: Attestation parameters live in one place
         run: python3 scripts/check_attest_params.py
+      - name: Every assumption the security rests on is registered
+        run: python3 tools/nonos-assumptions
+      - name: No new control that exists and does not run
+        run: python3 scripts/check_unenforced.py && python3 scripts/check_unenforced.py --self-test
+      - name: Linux syscall coverage does not fall
+        run: python3 tools/nonos-linux-coverage --baseline scripts/baselines/linux-syscalls.txt
+      - name: Wayland coverage does not fall
+        run: python3 tools/nonos-wayland-coverage --baseline scripts/baselines/wayland-globals.txt
+      - name: Every served Linux call says what it discloses
+        run: python3 tools/ratchets/disclosure.py
+      - name: Every mutant still removes the control it names
+        run: python3 tools/nonos-mutant --check
 
   # The committed verification/evidence/EVIDENCE.json is a machine-readable inventory of
   # everything NONOS proves. Regenerate it from the source tree and fail if it
@@ -343,6 +355,8 @@ jobs:
           - audio_proto_proofs
           - capsule_crypto_proofs
           - aes_proofs
+          - capsule_linux_proofs
+          - market_proofs
     steps:
       - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v4.2.2
         with:

.keys/marketplace_operator_ed25519.pub

@@ -0,0 +1,2 @@
+)_„É|b
<C‹Ê=Á€˜Ÿ
+;¡úâT­êŽc

Cargo.toml

@@ -113,6 +113,7 @@ nonos-capsule-video-player      = []
 nonos-capsule-about             = []
 nonos-capsule-install           = []
 nonos-capsule-install-cli       = []
+nonos-capsule-app-store         = []
 nonos-capsule-audio-player      = []
 nonos-capsule-hello             = []
 nonos-capsule-boot-splash       = []
@@ -556,6 +557,8 @@ microkernel-desktop-base = [
   "nonos-capsule-about",
   "nonos-capsule-install",
   "nonos-capsule-install-cli",
+  "nonos-capsule-app-store",
+  "nonos-capsule-market",
   "nonos-capsule-linux",
   "nonos-capsule-audio",
   "nonos-capsule-driver-hda",
@@ -873,7 +876,9 @@ x25519-dalek     = { version = "2",     default-features = false, features = ["s
 sha3             = { version = "0.10",  default-features = false, optional = true }
 
 # Hashing.
-blake3 = { version = "1.0",  default-features = false }
+# Portable only: the SSE and AVX assembly would use vector registers in the
+# kernel, which runs before a thread's are saved.
+blake3 = { version = "1.0",  default-features = false, features = ["pure"] }
 sha2   = { version = "0.10", default-features = false, features = ["force-soft"] }
 
 # Core utilities used in the kernel tree.
@@ -886,9 +891,6 @@ smoltcp = { version = "0.11", default-features = false, features = ["alloc", "so
 [target.'cfg(target_arch = "x86_64")'.dependencies]
 x86_64 = { version = "0.14", default-features = false, features = ["abi_x86_interrupt", "instructions"] }
 
-[target.'cfg(not(target_arch = "x86_64"))'.dependencies]
-blake3 = { version = "1.0", default-features = false, features = ["pure"] }
-
 [build-dependencies]
 blake3        = { version = "1.5",  default-features = false }
 cc            = "1.1"

Makefile

@@ -197,6 +197,11 @@ doctor:
 	else echo "  MISS  rust $(TOOLCHAIN)   (rustup toolchain install $(TOOLCHAIN))"; ok=0; fi; \
 	if [ -n "$(OVMF)" ] && [ -f "$(OVMF)" ]; then echo "  ok    OVMF $(OVMF)"; \
 	else echo "  MISS  OVMF UEFI firmware"; ok=0; fi; \
+	if ! $(QEMU) -accel help 2>/dev/null | grep -qx "$(QEMU_ACCEL)"; then \
+		echo "  MISS  accel $(QEMU_ACCEL)   ($(QEMU) does not offer it; set QEMU_ACCEL)"; ok=0; \
+	elif [ "$(QEMU_ACCEL)" = tcg ]; then \
+		echo "  ok    accel tcg   (no /dev/kvm or hvf: the CPU is emulated and boots are slow)"; \
+	else echo "  ok    accel $(QEMU_ACCEL)"; fi; \
 	echo; \
 	if [ $$ok = 1 ]; then echo "  This host can build and boot NONOS."; \
 	else \

abi/syscalls.toml

@@ -1,3 +1,10 @@
+# Each [desc.TAG] block publishes the gate the kernel applies to that call.
+# `caps = [...]` means all of the listed capabilities: a token needs every one.
+# `caps_any = [...]` means any one of them is enough. A block carries one field
+# or the other, never both. `caps = ["valid_token"]` means any valid token.
+# scripts/check_syscall_caps.py compares each block against the kernel's cap
+# table and fails on any difference, so a gate here is what the kernel enforces.
+
 version = 3
 abi = "nonos-sys-v1"
 
@@ -72,6 +79,9 @@ MFSP = 0x5053464D
 MFST = 0x5453464D
 MFWT = 0x5457464D
 MFRP = 0x5052464D
+MFCX = 0x5843464D
+MFSG = 0x4753464D
+MFIN = 0x4E49464D
 MPMP = 0x504D504D
 MPCP = 0x5043504D
 MPPT = 0x5450504D
@@ -84,6 +94,10 @@ MLSG = 0x47534C4D
 MLVF = 0x46564C4D
 MAIN = 0x4E49414D
 MDRO = 0x4F52444D
+MLCG = 0x47434C4D
+MLCR = 0x52434C4D
+MAPL = 0x4C50414D
+MAIS = 0x5349414D
 MIRW = 0x5752494D
 MIRY = 0x5952494D
 MKAR = 0x52414B4D
@@ -622,6 +636,24 @@ caps = ["ForeignExec"]
 args = [{name="pid",type="u32",dir="in"},{name="value",type="u64",dir="in"}]
 ret  = {type="i64"}
 
+[desc.MFCX]
+nr   = 0x5843464D
+caps = ["ForeignExec"]
+args = [{name="pid",type="u32",dir="in"},{name="out",type="u64*",dir="out"}]
+ret  = {type="i64"}
+
+[desc.MFSG]
+nr   = 0x4753464D
+caps = ["ForeignExec"]
+args = [{name="pid",type="u32",dir="in"},{name="regs",type="u64*",dir="in"},{name="kind",type="u64",dir="in"}]
+ret  = {type="i64"}
+
+[desc.MFIN]
+nr   = 0x4E49464D
+caps = ["ForeignExec"]
+args = [{name="pid",type="u32",dir="in"}]
+ret  = {type="i64"}
+
 [desc.MPMP]
 nr   = 0x504D504D
 caps = ["ForeignExec"]
@@ -637,7 +669,7 @@ ret  = {type="i64"}
 [desc.MFTH]
 nr   = 0x4854464D
 caps = ["ForeignExec"]
-args = [{name="pid",type="u32",dir="in"},{name="entry",type="u64",dir="in"},{name="rsp",type="u64",dir="in"},{name="tls",type="u64",dir="in"}]
+args = [{name="pid",type="u32",dir="in"},{name="entry",type="u64",dir="in"},{name="rsp",type="u64",dir="in"},{name="tls",type="u64",dir="in"},{name="from",type="u32",dir="in"}]
 ret  = {type="i64"}
 
 [desc.MPTL]
@@ -679,7 +711,7 @@ ret  = {type="i64"}
 [desc.MAIN]
 nr   = 0x4E49414D
 caps = ["AppInstall"]
-args = [{name="name_ptr",type="u64",dir="in"},{name="name_len",type="u64",dir="in"}]
+args = [{name="listing_ptr",type="u64",dir="in"},{name="listing_len",type="u64",dir="in"},{name="release_ptr",type="u64",dir="in"},{name="release_len",type="u64",dir="in"}]
 ret  = {type="i64"}
 
 [desc.MDRO]
@@ -688,6 +720,30 @@ caps = ["EnrolDevRoot"]
 args = []
 ret  = {type="i64"}
 
+[desc.MLCG]
+nr   = 0x47434C4D
+caps = ["EnrolDevRoot"]
+args = [{name="op",type="u64",dir="in"},{name="token_ptr",type="u8*",dir="out"}]
+ret  = {type="i64"}
+
+[desc.MLCR]
+nr   = 0x52434C4D
+caps = ["EnrolDevRoot"]
+args = [{name="token_ptr",type="u8*",dir="in"}]
+ret  = {type="i64"}
+
+[desc.MAIS]
+nr   = 0x5349414D
+caps = ["AppInstall"]
+args = [{name="listing_ptr",type="u64",dir="in"},{name="listing_len",type="u64",dir="in"}]
+ret  = {type="i64"}
+
+[desc.MAPL]
+nr   = 0x4C50414D
+caps = ["AppInstall"]
+args = [{name="listing_ptr",type="u64",dir="in"},{name="listing_len",type="u64",dir="in"}]
+ret  = {type="i64"}
+
 [desc.MPPT]
 nr   = 0x5450504D
 caps = ["ForeignExec"]

build.rs

@@ -570,7 +570,11 @@ fn rerun_on_capsule_binaries() {
 /// the whole space uniformly and needs neither.
 fn c_target(arch: &str) -> Option<(&'static str, &'static [&'static str])> {
     match arch {
-        "x86_64" => Some(("x86_64-unknown-none-elf", &["-mno-red-zone", "-mcmodel=kernel"][..])),
+        // No vector registers: kernel code runs before a thread's are saved.
+        "x86_64" => Some((
+            "x86_64-unknown-none-elf",
+            &["-mno-red-zone", "-mcmodel=kernel", "-mno-mmx", "-mno-sse", "-mno-sse2", "-mno-avx"][..],
+        )),
         "aarch64" => Some(("aarch64-unknown-none-elf", &[][..])),
         "riscv64" => Some(("riscv64-unknown-none-elf", &[][..])),
         _ => None,

mk/10-qemu.mk

@@ -44,17 +44,47 @@ endif
 
 QEMU_MEM := 2G
 QEMU_CPU := max
+# The accelerator follows the host, by the rule scripts/bootmatrix/qemu.py
+# already uses: KVM when /dev/kvm opens read-write, hvf on macOS, TCG
+# otherwise. TCG emulates the processor, so `-cpu host` names nothing there and
+# it gets `max`, which carries RDRAND. Set QEMU_ACCEL to override.
+ifeq ($(shell [ -r /dev/kvm ] && [ -w /dev/kvm ] && echo y),y)
+    QEMU_ACCEL_AUTO := kvm
+else ifeq ($(UNAME_S),Darwin)
+    QEMU_ACCEL_AUTO := hvf
+else
+    QEMU_ACCEL_AUTO := tcg
+endif
+QEMU_ACCEL ?= $(QEMU_ACCEL_AUTO)
+ifeq ($(QEMU_ACCEL),tcg)
+    QEMU_ACCEL_ARGS := -accel tcg -cpu $(QEMU_CPU)
+else
+    QEMU_ACCEL_ARGS := -accel $(QEMU_ACCEL) -cpu host,+rdrand,+rdseed
+endif
 QEMU_SMP ?= 4
 QEMU_HOST_SSH_PORT ?= 2222
 QEMU_HOST_HTTP_PORT ?= 8080
 QEMU_NET_MODE ?= nat
-QEMU_NET_CAPTURE ?=
+# Every networked run is captured, so what a boot sent is on disk rather than
+# inferred from the code; tools/nonos-pcap-egress summarises it. Set it empty
+# to run without one.
+QEMU_NET_CAPTURE ?= $(TARGET_DIR)/qemu-net.pcap
 QEMU_SERIAL_LOG ?= $(TARGET_DIR)/qemu-serial.log
 QEMU_SMP_SERIAL_LOG ?= $(TARGET_DIR)/qemu-smp-serial.log
 QEMU_IOMMU_SERIAL_LOG ?= $(TARGET_DIR)/qemu-iommu-serial.log
 # Options for the intel-iommu device the IOMMU lane adds; a knob like the
 # others so the lane can be driven from the command line.
 QEMU_IOMMU_OPTS ?= intremap=on,caching-mode=on
+# A virtio device uses the vIOMMU only with iommu_platform=on, and only then is
+# VIRTIO_F_ACCESS_PLATFORM offered. Without it the device addresses memory
+# physically and the lane tests nothing about it. disable-legacy=on because a
+# legacy driver cannot take bit 33: it fails to bind instead of bypassing.
+QEMU_IOMMU_VIRTIO ?= iommu_platform=on,disable-legacy=on
+_iv := $(_boot_comma)$(QEMU_IOMMU_VIRTIO)$(_boot_comma)
+iommu_virtio = $(foreach d,virtio-blk-pci virtio-net-pci virtio-rng-pci virtio-vga virtio-vga-gl,\
+	$(eval _iommu_args := $(patsubst $(d),$(d)$(_boot_comma)$(QEMU_IOMMU_VIRTIO),\
+	$(subst $(d)$(_boot_comma),$(d)$(_iv),$(_iommu_args)))))$(_iommu_args)
+iommu_virtio_args = $(eval _iommu_args := $(subst virtio-vga$(_boot_comma)disable-modern=on,virtio-vga,$(1)))$(call iommu_virtio)
 QEMU_BLK_IMG := $(TARGET_DIR)/qemu-virtio-blk.img
 QEMU_OVMF_VARS_RW := $(TARGET_DIR)/qemu-OVMF_VARS.fd
 QEMU_BLK := -drive "file=$(QEMU_BLK_IMG),if=none,id=vd0,format=raw" -device virtio-blk-pci,drive=vd0
@@ -84,19 +114,29 @@ QEMU_YRES ?= 1080
 # QEMU_GL=1 swaps the display device for virtio-vga-gl (modern transport,
 # virglrenderer backend) so the guest can negotiate the 3D command set; the
 # cocoa display then needs a GL context. Default stays the plain 2D device.
+# cocoa exists only on macOS; elsewhere the window is gtk.
+ifeq ($(UNAME_S),Darwin)
+QEMU_UI := cocoa
+else
+QEMU_UI := gtk
+endif
 ifeq ($(QEMU_GL),1)
 QEMU_GPU := -device virtio-vga-gl,xres=$(QEMU_XRES),yres=$(QEMU_YRES)
-QEMU_DISPLAY := cocoa,gl=es,zoom-to-fit=on
+QEMU_DISPLAY ?= $(QEMU_UI),gl=es,zoom-to-fit=on
 else
 QEMU_GPU := -device virtio-vga,disable-modern=on,vectors=0,edid=on,xres=$(QEMU_XRES),yres=$(QEMU_YRES)
-QEMU_DISPLAY := cocoa,zoom-to-fit=on
+QEMU_DISPLAY ?= $(QEMU_UI),zoom-to-fit=on
 endif
 # Keyboard/mouse via the q35 i8042 (PS/2). USB HID interrupt-IN transfers
 # are not serviced under macOS hvf, so usb-kbd/usb-mouse never deliver input
 # there; the xHCI controller stays for the USB stack/storage paths.
 QEMU_USB := -device qemu-xhci,id=xhci
 QEMU_RNG := -device virtio-rng-pci
+ifeq ($(UNAME_S),Darwin)
 QEMU_AUDIODEV ?= coreaudio
+else
+QEMU_AUDIODEV ?= none
+endif
 QEMU_AUDIO := -audiodev $(QEMU_AUDIODEV),id=snd0 -device intel-hda -device hda-duplex,audiodev=snd0
 
 # Software TPM 2.0 for measured boot. The guest reaches it by direct MMIO at