Skip to content

linux: finish the stack (#532 #535 #512 + install queue) - #559

Merged
senseix21 merged 24 commits into
mainfrom
integ/linux-finish
Sep 26, 2026
Merged

senseix21 merged 24 commits into
mainfrom
integ/linux-finish

Conversation

@senseix21

@senseix21 senseix21 commented Sep 26, 2026 •

Copy link
Copy Markdown
Collaborator

Finishes the Linux stack.

#532, #535 and #512 each depend on another in a cycle, so none of them can merge on its own:

This branch merges them in that order on top of main. Each one is a real merge commit, so GitHub closes #532, #535 and #512 as merged.

Also in this PR

Local gates

  • syscall-abi: 105 syscalls, all reach a handler.
  • caps-abi: 34 bits agree.
  • userland-caps and cap-parity: agree.
  • allows, unreachable, stubs: 0 new.

eKisNonos and others added 19 commits September 20, 2026 12:00
Capability was written out three times. bits_to_caps filters over
all(), so an entry missing there is grantable in a signed manifest and
resolves to nothing at spawn. That is how ForeignExec went missing.

capability_table! generates the enum, bit(), all() and count() from
defs.rs. bit.rs and all.rs are deleted. guard.rs fails the build if
two capabilities share a bit.

IO and Hardware enforce nothing: their only readers are can_read,
can_write and can_hardware, none of which is called. Both documented
as such, naming what really gates each thing.

cap-audit counted any mention of Capability::X as a consultation,
including inside dead checkers, which is why it passed. It resolves
each checker to whether anything calls it now, with IO and Hardware
as a recorded baseline so the list can only shrink.
MkLocalSign was gated on can_admin. Nothing requests Admin and it is
in FORBIDDEN_AMBIENT, so vouch always failed: every package the Linux
installer wrote had no trailer, and the exec gate then refused it.

LocalSign gets its own bit. Admin is keys to everything including
MkCapGrant, EnrolDevRoot is a different job, and AppInstall would let
a capsule decide what the machine runs as a side effect of installing.

Five of the seven places that must agree are here. The Linux manifest
and its spawn mirror land with the personality.

Trailer verification dispatches on the trailer's magic rather than
nonos-stark-attest. Following the flag meant a local mint produced
NZKCAPS2 while the verifier expected NZKSTRK1, and it surfaced as a
malformed trailer rather than a configuration error.

cap_table's doc says it is an entry gate, not the authority map. Two
reviews have read it the other way and called the handlers unguarded.
Zero capabilities was being treated as containment. brk, munmap and
the wayland shm path took a guest number and acted on it, so a guest
could unmap the personality or ask for a buffer no machine has. Limits
come from one address plan in guest/layout.rs now. They had already
drifted: only map.rs knew the mapping cursor's neighbour is EXEC_BASE
and not the stack.

Paths resolve to a Key only file::resolve can mint and the store
wrappers take nothing else, so /linux is the root by construction.

PT_INTERP and library mappings were loaded unproven, which left the
attestation gate on the main image doing nothing useful. Both proven,
ELF arithmetic checked. argv was read under MAX_PATH, so long
arguments failed execve with nothing saying why.

The resolver hands out 100.64/10 addresses and maps them back at
connect, and the installer runs over the mixnet. resolve_host in
net_sockets still does a clearnet lookup and is not fixed here.

Package bytes are still unauthenticated, so place_entry refuses to
vouch for them and the exec gate refuses what lands.

tar::entries stopped at the first end-of-archive block, which in an
apk is the end of the signature stream, so unpack had never written a
file. Mirrored in python: one stream, sig+ctl+data, unterminated
middle, garbage tail.
A runtime installs handlers before main and checks the return. Answering
ENOSYS made programs abort at startup that would otherwise have run to
completion, because most of them never raise anything.

rt_sigaction, rt_sigprocmask and sigaltstack now succeed and record what
was asked. Nothing is ever raised. Delivery means pushing a frame onto a
guest thread's stack and redirecting it, and the trap mechanism hands out
a register frame without any way to rewrite one, so it cannot be done
from here yet.

That limit is written in the file rather than hidden behind the success:
a program that depends on SIGALRM will hang rather than misbehave
quietly, which is the failure that can be diagnosed. SIGKILL and SIGSTOP
are refused as uncatchable, as Linux refuses them.
net.sockets offers socket, connect, send, recv, close and a readiness
poll, keyed by the caller's pid, which maps onto the Linux calls almost
one to one. A guest's descriptor now holds a handle that service issued
to this capsule, so a guest reaches only the sockets opened for it.

read and write route by descriptor kind, so a program that treats a
socket as a file, which most do, works without knowing the difference.
Closing one closes the handle behind it.

poll answers for every descriptor. A file or a console is always ready,
which is what Linux reports too. A socket is asked one handle at a time,
because that is the shape of the readiness call the service serves, and
inventing a batched form here would mean a second protocol with nobody
on the other end.

The opcodes are transcribed rather than imported: the server is a binary
and its protocol module is not a library. The file they came from is
named beside them, since a number that changes there and not here is a
wrong operation rather than a failed one.
supervised_asid returned an asid and dropped the lock that made it
true, so peer map, unmap, copy and protect all ran against an asid the
supervisor no longer held. It returns the guard with it now.

The entry stub saves the callee-saved five plus a pad so a forked
child resumes on the parent's register state. Nothing else on the path
writes them to memory and a handler's prologue may already be using
them, so it happens in the stub or not at all. Six slots keeps the
frame 16-byte aligned and leaves existing offsets alone.

libc gains wrappers for foreign exec, fork and resume, peer TLS and
unmap, and the local signing and consent calls.
# Conflicts:
#	src/capabilities/types/as_str.rs
#	src/capabilities/types/bit.rs
#	src/capabilities/types/defs.rs
bit.rs and all.rs are gone: every capability's bit now sits beside its
name in types/defs.rs, and table.rs generates bit(), all() and count()
from it. Three consumers still read the deleted files. The two ABI
checkers parse defs.rs's `Name = 1 << n` entries instead of bit.rs's
match arms; attest_receipt includes table.rs and guard.rs in place of
bit.rs and all.rs; and kernel_proofs binds by value in the loops over
all(), which now yields a static slice rather than an owned array.

Refs #532
pr535 is a single commit made on a stale tree: taken whole it re-added the
five signing calls 1aeddc6 removed (CEDV/CEDS/CEDP/CSKS/CSPB), dropped
CryptoMachineKey, and reverted comment work in the syscall tables. The
syscall-table files are resolved as main plus only the new numbers
(MPTL MFFK MPUN MFEX MLSG MLVF MAIN MDRO), their dispatch, their gates and
can_local_sign/can_app_install. MPTL..MFEX resolve once #512 lands.
de5a310 carried stale copies of abi/syscalls.toml and the libc export
lists: taken whole they re-added the removed ed25519/secp256k1 calls,
dropped CryptoMachineKey and undid the per-call capabilities of ac000a8
and a0d26d0. Those three files are resolved as main plus the new calls
only (MPTL MFFK MPUN MFEX MLSG MLVF MAIN MDRO, their libc wrappers and
numbers); the toml now also describes the four #535 numbers.
MkAppInstall (#535) hands a package name to init::request_install, which
only #545 defined, alongside the App Store capsule and a marketplace index
that must be signed into nonos-data. Only the queue is taken: a bounded,
deduplicated list that init's supervisor loop drains through
capsule_linux::spawn_install. #545's wake/priority rework is left out; the
loop already parks for at most 20 ms, which bounds how long a request waits.
58eec9d deferred release_new until something called it. #512's
foreign start_context is that caller: a guest whose stack or first
context fails to build after claim_new must go back to New, or the pid
stays claimed and can never be started.
#512 re-exports registry::is_foreign, which f3fb4af deferred until it
had a caller. park()'s recheck is that caller: it only asks whether the
guest is still in the table, not who supervises it.
LocalSign (bit 33) is enforced by the kernel but was missing from
abi/caps.toml, and MDRO published EnrolDevRoot while the cap table
routes it through the same arm as MDRQ/MDRC, which the syscall-ABI gate
reads as valid_token. The authority check stays inside the handler.
The kernel defines 34 capabilities after LocalSign landed, but the shell
and terminal name tables, nonos_cap and the manifest parser stopped at
ForeignExec, so a manifest could not name it and the UIs printed an
unnamed bit.
The stub gate reads 'entry stub' as an admission of unsupported work.
The assembly entry is complete; say what it is so the baseline need not
grow.
The linux merges add userland/capsule_linux_proofs, so the regenerated
evidence counts 55 runnable proof crates and CI's drift check fails
against the committed 54.
eKisNonos and others added 5 commits September 26, 2026 12:48
syscall.S saves 17 words and frame_snapshot read 16, so a forked child
got a kernel stack word in rbx and lost r15. The size now lives in
syscall_frame.inc; syscall.S checks its saves against it and Rust reads it.
Every foreign handler takes its pid through pid_arg, which refuses a value
past u32 instead of letting 2^32 + n name process n.
#532 moved Capability::bit from types/bit.rs into the generated table in
defs.rs as a shift, and #532 added LocalSign at bit 33. The extraction
gate regenerated Caps.lean and found drift; this is its output, and the
refinement proofs follow the renamed path and index the new variant.
The one-list table computes each bit as a shift, so per-case rfl no longer
unfolds has_capability and add_capability to a literal. Both now take the
bit's value from bit_spec, which still closes per case, and are uniform over
the variants instead of enumerating them.
@senseix21

Copy link
Copy Markdown
Collaborator Author

@eKisNonos Review before merge (update)

Scope
Incremental diff 1048746..7544163: merge of origin/main (#560 zk group order, #561 caps checker fails closed) and merge of linux/frame-words-pid-arg (de43688).

Our changes

  • Both merges were textually clean; no conflict hunks.
  • One semantic fix folded into the second merge: abi/syscalls.toml [desc.MDRO] caps ["valid_token"] -> ["EnrolDevRoot"]. With abi: fail the caps check closed and publish the hardware gates #561's fail-closed checker, check_syscall_abi.py rejected the old row because the cap table now demands EnrolDevRoot (can_enrol_dev_root). Caps.lean / Refinement.lean / cap mirrors: linux: finish the stack (#532 #535 #512 + install queue) #559's versions kept (ek's branch did not re-touch them in a way that conflicted).
  • Local gates: 14/14 argument-free scripts/check_*.py pass (incl. check_syscall_caps.py, check_syscall_abi.py); the other 2 (check_declared_caps, check_staged_kernel) need artifact args. Kernel cargo check (x86_64-nonos) and capsule_linux user-target cargo check clean. collect-evidence.sh produced no EVIDENCE.json drift.

Findings

  • FRAME_WORDS: syscall.S counts saves via SAVE/SAVE_PAD macros: r15 r14 r13 r12 rbx (5) + 2 pads + rdx rsi rdi rbp r11 rcx r10 r9 r8 rax (10) = 17 = SYSCALL_FRAME_WORDS in syscall_frame.inc; .if FRAME_SAVED != SYSCALL_FRAME_WORDS / .error is present. frame_snapshot.rs takes &[u64; FRAME_WORDS] with rbx..r15 at FRAME_WORDS-5..-1, plus a const assert RDX < RBX. Correct; fixes the 16-vs-17 off-by-one (rbx read a kernel word, r15 lost).
  • Pid checks: all 10 foreign handlers go through pid_arg (u32::try_from, EINVAL on overflow) before any use: exec, fork, peer_tls, spawn_start, thread, trap_reply directly; peer_copy, peer_map, peer_protect, peer_unmap via supervised_asid, whose first step is pid_arg(pid)?. No as u32 casts remain in src/process/foreign.
  • MDRO: cap_table/mk.rs gates MkDevRootLocal on caps.can_enrol_dev_root() (= Capability::EnrolDevRoot); TOML row now matches.
  • No blockers.

Verdict: holding for boot verification.

@senseix21

Copy link
Copy Markdown
Collaborator Author

@eKisNonos Boot verification of head 75441634d passed. Booted under QEMU/hvf with make nonos-mk-run.

  • Attestation and faults: 68 capsules spawned. 0 [ZK-ATTEST] FAIL. 0 #GP, #PF or EXCEPTION.
  • Linux and install capsules: app.linux and installer both spawned and attested.
  • Desktop and Terminal: the desktop comes up, the dock shows the Install icon, and the Terminal opens. git init and git status run correctly.

Verdict: merging. CI was green on this head: ci, verify, lean and boot-smoke.

@senseix21
senseix21 merged commit 3165901 into main Sep 26, 2026
66 of 121 checks passed
eKisNonos added a commit that referenced this pull request Sep 27, 2026
#562's init boost is kept in the branch's instance_spawn::priority form,
which masks interrupts around the lock; main's entry.rs guard is kept.
The ABI table takes main's caps_any order; every ABI check passes.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants