Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
24 commits
Select commit Hold shift + click to select a range
3bc3c88
capabilities: generate the enum, bit and all from one list
eKisNonos Sep 20, 2026
5a678d9
syscall: give local signing a capability a capsule can hold
eKisNonos Sep 20, 2026
747edf5
linux: confine the guest and prove what it is asked to run
eKisNonos Sep 20, 2026
23a1b4a
linux: record a signal disposition, and never claim to deliver one
eKisNonos Sep 18, 2026
6b25519
linux: sockets and poll, over the service that already has them
eKisNonos Sep 18, 2026
de5a310
process: hold the supervised asid for the length of the call
eKisNonos Sep 20, 2026
597fd42
Merge remote-tracking branch 'origin/main' into caps/one-list
senseix21 Sep 24, 2026
b497dc3
Merge remote-tracking branch 'origin/main' into caps/one-list
senseix21 Sep 24, 2026
dec4381
fix(caps): point the table's consumers at the one list
senseix21 Sep 24, 2026
07b1735
Merge branch 'pr532' into integ/linux-finish
senseix21 Sep 26, 2026
6812c2d
Merge branch 'pr535' into integ/linux-finish
senseix21 Sep 26, 2026
771ff7e
Merge branch 'pr512' into integ/linux-finish
senseix21 Sep 26, 2026
f9aa0e2
feat(init): queue app installs for the linux installer
senseix21 Sep 26, 2026
5883548
fix(process): restore release_new for the guest start path
senseix21 Sep 26, 2026
cd02d65
fix(foreign): restore is_foreign for the park recheck
senseix21 Sep 26, 2026
c9798ad
fix(abi): publish LocalSign and the MDRO cap row the table demands
senseix21 Sep 26, 2026
3200125
fix(caps): mirror LocalSign in the userland cap tables
senseix21 Sep 26, 2026
54ba011
fix(syscall): name the syscall.S entry without the word stub
senseix21 Sep 26, 2026
a0c6100
fix(evidence): count the capsule_linux proof crate
senseix21 Sep 26, 2026
de43688
process: one frame size for syscall.S, and refuse a truncated pid
eKisNonos Sep 26, 2026
04a4ca6
fix(verification): regenerate the caps extraction for the one-list table
senseix21 Sep 26, 2026
1048746
fix(verification): prove the cap specs through bit_spec
senseix21 Sep 26, 2026
df3c93a
Merge origin/main into integ/linux-finish
senseix21 Sep 26, 2026
7544163
Merge linux/frame-words-pid-arg into integ/linux-finish
senseix21 Sep 26, 2026
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
The table of contents is too big for display.
Diff view
Diff view
  •  
  •  
  •  
1 change: 1 addition & 0 deletions abi/caps.toml
Original file line number Diff line number Diff line change
Expand Up @@ -36,6 +36,7 @@ ENTROPY = 0x0000_0000_2000_0000
APP_INSTALL = 0x0000_0000_4000_0000
ATTEST_READ = 0x0000_0000_8000_0000
FOREIGN_EXEC = 0x0000_0001_0000_0000
LOCAL_SIGN = 0x0000_0002_0000_0000

# Named bundles, each the set a class of capsule is actually spawned with in
# this tree. They named LOG, YIELD, TIME and KSTAT until now, which are not
Expand Down
56 changes: 56 additions & 0 deletions abi/syscalls.toml
Original file line number Diff line number Diff line change
Expand Up @@ -76,6 +76,14 @@ MPMP = 0x504D504D
MPCP = 0x5043504D
MPPT = 0x5450504D
MFTH = 0x4854464D
MPTL = 0x4C54504D
MFFK = 0x4B46464D
MPUN = 0x4E55504D
MFEX = 0x5845464D
MLSG = 0x47534C4D
MLVF = 0x46564C4D
MAIN = 0x4E49414D
MDRO = 0x4F52444D
MIRW = 0x5752494D
MIRY = 0x5952494D
MKAR = 0x52414B4D
Expand Down Expand Up @@ -632,6 +640,54 @@ 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"}]
ret = {type="i64"}

[desc.MPTL]
nr = 0x4C54504D
caps = ["ForeignExec"]
args = [{name="pid",type="u32",dir="in"},{name="base",type="u64",dir="in"}]
ret = {type="i64"}

[desc.MFFK]
nr = 0x4B46464D
caps = ["ForeignExec"]
args = [{name="pid",type="u32",dir="in"}]
ret = {type="i64"}

[desc.MPUN]
nr = 0x4E55504D
caps = ["ForeignExec"]
args = [{name="pid",type="u32",dir="in"},{name="addr",type="u64",dir="in"},{name="len",type="u64",dir="in"}]
ret = {type="i64"}

[desc.MFEX]
nr = 0x5845464D
caps = ["ForeignExec"]
args = [{name="pid",type="u32",dir="in"},{name="entry",type="u64",dir="in"},{name="rsp",type="u64",dir="in"}]
ret = {type="i64"}

[desc.MLSG]
nr = 0x47534C4D
caps = ["LocalSign"]
args = [{name="elf_ptr",type="u64",dir="in"},{name="elf_len",type="u64",dir="in"},{name="caps",type="u64",dir="in"},{name="out_ptr",type="u64",dir="out"},{name="out_len",type="u64",dir="in"}]
ret = {type="i64"}

[desc.MLVF]
nr = 0x46564C4D
caps = ["ForeignExec"]
args = [{name="elf_ptr",type="u64",dir="in"},{name="elf_len",type="u64",dir="in"},{name="caps",type="u64",dir="in"},{name="trailer_ptr",type="u64",dir="in"},{name="trailer_len",type="u64",dir="in"}]
ret = {type="i64"}

[desc.MAIN]
nr = 0x4E49414D
caps = ["AppInstall"]
args = [{name="name_ptr",type="u64",dir="in"},{name="name_len",type="u64",dir="in"}]
ret = {type="i64"}

[desc.MDRO]
nr = 0x4F52444D
caps = ["EnrolDevRoot"]
args = []
ret = {type="i64"}

[desc.MPPT]
nr = 0x5450504D
caps = ["ForeignExec"]
Expand Down
6 changes: 3 additions & 3 deletions scripts/check_cap_parity.py
Original file line number Diff line number Diff line change
Expand Up @@ -33,7 +33,7 @@
import sys
from pathlib import Path

KERNEL_BITS = Path("src/capabilities/types/bit.rs")
KERNEL_BITS = Path("src/capabilities/types/defs.rs")
USER_BITS = Path("userland/nonos_cap/src/bits.rs")
MANIFEST_BITS = Path("userland/platform/nonos_manifest/src/caps/bit.rs")

Expand All @@ -51,8 +51,8 @@ def canonical(name: str) -> str:

def read_kernel(root: Path):
text = (root / KERNEL_BITS).read_text()
pairs = re.findall(r"Self::(\w+)\s*=>\s*(\d+)\s*,", text)
return {canonical(n): int(v) for n, v in pairs}
pairs = re.findall(r"^\s*(\w+)\s*=\s*1\s*<<\s*(\d+)\s*,", text, re.M)
return {canonical(n): 1 << int(v) for n, v in pairs}


def read_userland(root: Path):
Expand Down
8 changes: 4 additions & 4 deletions scripts/check_caps_abi.py
Original file line number Diff line number Diff line change
Expand Up @@ -18,7 +18,7 @@

`abi/caps.toml` is what an external toolchain reads to learn what a capability
bit means. The kernel is the only thing that decides that, so the file is
correct exactly when it agrees with `src/capabilities/types/bit.rs`.
correct exactly when it agrees with `src/capabilities/types/defs.rs`.

The existing CI check compares four graphics entries against values written
into the check itself, which makes the check a third copy of the table rather
Expand All @@ -36,7 +36,7 @@
import sys
from pathlib import Path

KERNEL_BITS = Path("src/capabilities/types/bit.rs")
KERNEL_BITS = Path("src/capabilities/types/defs.rs")
ABI_CAPS = Path("abi/caps.toml")


Expand All @@ -46,8 +46,8 @@ def canonical(name: str) -> str:

def read_kernel(root: Path):
text = (root / KERNEL_BITS).read_text()
pairs = re.findall(r"Self::(\w+)\s*=>\s*(\d+)\s*,", text)
return {canonical(n): (n, int(v)) for n, v in pairs}
pairs = re.findall(r"^\s*(\w+)\s*=\s*1\s*<<\s*(\d+)\s*,", text, re.M)
return {canonical(n): (n, 1 << int(v)) for n, v in pairs}


def sections(text: str):
Expand Down
2 changes: 1 addition & 1 deletion src/arch/x86_64/asm/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -18,4 +18,4 @@ mod start;
mod syscall;

pub use start::_start;
pub use syscall::syscall_entry_asm;
pub use syscall::{syscall_entry_asm, SYSCALL_FRAME_WORDS};
79 changes: 66 additions & 13 deletions src/arch/x86_64/asm/syscall.S
Original file line number Diff line number Diff line change
Expand Up @@ -14,6 +14,18 @@
.set USER_CS, 0x23
.set USER_DS, 0x1B

#include "syscall_frame.inc"

.set FRAME_SAVED, 0
.macro SAVE reg
push \reg
.set FRAME_SAVED, FRAME_SAVED + 1
.endm
.macro SAVE_PAD
sub rsp, 8
.set FRAME_SAVED, FRAME_SAVED + 1
.endm

syscall_entry_asm:
swapgs
/* Rust and C string/memory code require DF=0 even if user RFLAGS had DF set. */
Expand All @@ -27,17 +39,34 @@ syscall_entry_asm:
below destroys them, so stash the user copies under the saved frame and
restore them on exit. One pad slot keeps 16-alignment since three
arg-saves are odd. Eleven slots -> rsp = 8 (mod 16). */
sub rsp, 8
push rdx
push rsi
push rdi
push rbp
push r11
push rcx
push r10
push r9
push r8
push rax
/* The callee-saved five, plus a pad to keep the parity the comment
above depends on. Nothing else on this path writes them to memory,
and Rust cannot read them either: by the time a handler runs, its
own prologue may already be using them. A forked child has to
resume with the parent's whole register state, so the capture has
to happen here or not at all. Six slots is 0 (mod 16), so every
offset below stays exactly where it was. */
SAVE r15
SAVE r14
SAVE r13
SAVE r12
SAVE rbx
SAVE_PAD

SAVE_PAD
SAVE rdx
SAVE rsi
SAVE rdi
SAVE rbp
SAVE r11
SAVE rcx
SAVE r10
SAVE r9
SAVE r8
SAVE rax
.if FRAME_SAVED != SYSCALL_FRAME_WORDS
.error "syscall frame: the words saved disagree with SYSCALL_FRAME_WORDS"
.endif

/* User ABI -> SysV: nr,a1..a6. rdi/rsi/rdx still hold the user args here.
The frame offsets match the original 7-push layout because the arg-saves
Expand All @@ -50,10 +79,23 @@ syscall_entry_asm:
mov r9, [rsp + 0x08]
mov r11, [rsp + 0x10]

/* Spill a6 as 7th arg, realigns to 16. */
/* a6 goes on the stack as the seventh argument; the eighth is a
pointer to the frame just saved. A pointer rather than a single
register because a forked child resumes with the parent's whole
state, and the frame holds all of it: the return address is the
saved rcx at offset 0x20 and the rest follows it. Taken before
the two pushes, so it points at the saved rax.

One push left rsp 16-aligned for the call. Two do not, so a pad goes
underneath them: the arguments themselves must sit at [rsp] and
[rsp+8] when the call executes. Cleanup grows from 0x10 to 0x20 for
the pad and the extra argument. */
mov rax, rsp
sub rsp, 8
push rax
push r11
call syscall_handler
add rsp, 0x10
add rsp, 0x20

/* SyscallSavedFrame{rax, r8, r9, r10, rcx, r11, rbp} at rsp. */
push rax
Expand All @@ -80,6 +122,17 @@ syscall_entry_asm:
pop rdx
add rsp, 8

/* The callee-saved five come back with their pad, in reverse. They
still hold the user's values, so this restores rather than
changes them; the point of saving was to give a supervisor a
complete frame to fork from. */
add rsp, 8
pop rbx
pop r12
pop r13
pop r14
pop r15

push rax
movabs rax, 0xffffffffffe08aff
and r11, rax
Expand Down
27 changes: 27 additions & 0 deletions src/arch/x86_64/asm/syscall.rs
Original file line number Diff line number Diff line change
Expand Up @@ -18,3 +18,30 @@
extern "C" {
pub fn syscall_entry_asm();
}

/// Words the entry code saves before it calls the handler, read from the file
/// the entry code itself assembles against, so the two cannot disagree.
pub const SYSCALL_FRAME_WORDS: usize = set_value(include_str!("syscall_frame.inc"));

/*
* The value after the last comma of the `.set` line. A file this does not
* parse fails the build here rather than yielding a wrong count.
*/
const fn set_value(text: &str) -> usize {
let b = text.as_bytes();
let mut i = b.len();
while i > 0 && !b[i - 1].is_ascii_digit() {
i -= 1;
}
let end = i;
while i > 0 && b[i - 1].is_ascii_digit() {
i -= 1;
}
assert!(i < end && i > 0 && b[i - 1] == b' ', "syscall_frame.inc: no count");
let mut n = 0;
while i < end {
n = n * 10 + (b[i] - b'0') as usize;
i += 1;
}
n
}
4 changes: 4 additions & 0 deletions src/arch/x86_64/asm/syscall_frame.inc
Original file line number Diff line number Diff line change
@@ -0,0 +1,4 @@
/* Words the syscall entry code leaves on the kernel stack before it calls the
* handler. The entry code counts its own saves against this and refuses to
* assemble on a mismatch; asm/syscall.rs reads the same line for Rust. */
.set SYSCALL_FRAME_WORDS, 17
23 changes: 12 additions & 11 deletions src/arch/x86_64/syscall/manager/entry.rs
Original file line number Diff line number Diff line change
Expand Up @@ -17,6 +17,7 @@
use crate::security::hardening::speculation::kernel_entry;
use crate::syscall::contract::{dispatch as contract_dispatch, SyscallArgs};
use crate::syscall::numbers::SyscallNumber;
use crate::process::foreign::FRAME_WORDS;
use crate::syscall::types::errnos;

#[no_mangle]
Expand All @@ -28,24 +29,24 @@ pub(super) extern "C" fn syscall_handler(
arg4: u64,
arg5: u64,
arg6: u64,
frame: *const u64,
) -> u64 {
// A capsule reaching this point last controlled the branch predictors and
// the return stack. Refilling the RSB and re-asserting IBRS before any
// kernel branch runs is the whole point of the entry side, and it was the
// side with no caller: `kernel_exit` was wired on the return path, so
// mitigations were being applied leaving the kernel but not entering it.
// the return stack.
kernel_entry();

let Some(sc) = SyscallNumber::from_u64(number) else {
// A number this kernel does not know.
let args = [arg1, arg2, arg3, arg4, arg5, arg6];
/*
* A number this kernel does not know. NONOS numbers are four
* character tags, so nothing legitimate lands here; a foreign
* binary's own numbering does. When the caller is a guest, its
* supervisor answers and the kernel stays ignorant of what was
* asked. Everyone else still gets ENOSYS.
* SAFETY: `frame` is the rsp the entry code took after its last save,
* so it points at FRAME_WORDS eight-byte words it pushed on this kernel
* stack; syscall.S refuses to assemble if it saves any other number.
* They stay live and untouched until this call returns, and nothing
* downstream of this reference is unsafe.
*/
let args = [arg1, arg2, arg3, arg4, arg5, arg6];
return match crate::process::foreign::redirect(number, args, 0) {
let saved = unsafe { &*(frame as *const [u64; FRAME_WORDS]) };
return match crate::process::foreign::redirect(number, args, saved) {
Some(value) => value,
None => (-(errnos::ENOSYS as i64)) as u64,
};
Expand Down
2 changes: 1 addition & 1 deletion src/capabilities/bits.rs
Original file line number Diff line number Diff line change
Expand Up @@ -27,7 +27,7 @@ pub fn caps_to_bits(caps: &[Capability]) -> u64 {

#[inline]
pub fn bits_to_caps(bits: u64) -> Vec<Capability> {
Capability::all().into_iter().filter(|c| bits & c.bit() != 0).collect()
Capability::all().iter().copied().filter(|c| bits & c.bit() != 0).collect()
}

#[inline]
Expand Down
62 changes: 0 additions & 62 deletions src/capabilities/types/all.rs

This file was deleted.

Loading
Loading