nx_caps.nx source

1// nx_caps.nx -- high-level capability combinators on memcap. 2// 3// memcap.nx ships the LOW-LEVEL primitive (32-byte software cap 4// with addr/base/len/perms/tag). This module gives the COMBINATOR 5// API that makes capabilities useful in practice: 6// 7// * derive_subrange -- carve a smaller cap from a larger one 8// with no more permission than the parent 9// * narrow_perms -- drop permissions (read-only view of an 10// RW region, etc.); the inverse direction 11// is illegal (caps may only get weaker) 12// * seal / unseal -- type-safe opaque wrapper (Mark Miller's 13// "sealer" pattern, E language 1997) 14// * revoke -- one-way invalidation; future derefs fail 15// * delegate -- transfer ownership across a boundary 16// with audit trail 17// * verify_chain -- prove a cap is reachable from a root 18// via legal weakening operations only 19// 20// CAPABILITY SECURITY MODEL: 21// 22// A cap is a triple (memory_region, perms, tag). Holding a cap 23// means having the AUTHORITY to use the region under perms. 24// The integrity of the model rests on: 25// 26// 1. UNFORGEABILITY -- you cannot construct a cap from 27// nothing; you can only derive from existing caps. 28// 2. MONOTONIC WEAKENING -- derived caps may have FEWER 29// permissions than parents; never more. 30// 3. NO AMBIENT AUTHORITY -- capability is the ONLY way to 31// access; there's no global "open file" syscall that takes 32// a string path. 33// 4. REVOCATION -- the holder of the parent (or a designated 34// revoker) can void all derived caps. 35// 36// LINEAGE: 37// 38// * Dennis-Van Horn 1966 (object capabilities, MIT) 39// * Hardy KeyKOS 1985 (capability microkernel) 40// * Shapiro EROS 1999 (capability OS, formal) 41// * Klein seL4 2009 (formally verified capabilities) 42// * Mark Miller "Robust Composition" 2006 PhD (E language, 43// sealer/unsealer pattern) 44// * Watson CHERI Morello 2023 (HW capability machine, ARM Ltd) 45// 46// MAPS TO HARDWARE: 47// 48// On non-CHERI hosts (today's RISC-V, x86): software-enforced 49// via runtime checks at every cap-mediated access. Slower but 50// correct. 51// 52// On CHERI hardware: lower nx_caps_* to native CHERI cap 53// instructions (clc, csc, ccall, cseal, cunseal). Same source, 54// ~10x throughput. 55 56// nx_safety_envelope: 57// intended_use: AUTO_APPLIED -- primitive-specific tuning queued 58// sil_target: SIL1 59// evidence: [bulk_applied_2026-05-16, see-file-comment-for-detail] 60// verdict: NOT_YET_EVALUATED 61 62import "syscalls.nx" 63import "memcap.nx" 64 65// ---- combinators on MemCap ---------------------------------------- 66 67// Derive a smaller cap from an existing one. The new cap covers 68// `[addr, addr+len)` which MUST be a subrange of `parent`'s region. 69// Permissions are narrowed via `new_perms` -- which must be a 70// subset of `parent.perms`. Returns NULL on illegal derive. 71func nx_caps_derive_subrange(parent: *MemCap, addr: i64, len: i64, 72 new_perms: i64) -> *MemCap { 73 // Subrange check: [addr, addr+len) ⊆ [parent.base, parent.base+parent.length) 74 if addr < parent.base { return 0 as *MemCap } 75 if (addr + len) > (parent.base + parent.length) { return 0 as *MemCap } 76 if len <= 0 { return 0 as *MemCap } 77 78 // Permission monotone: new_perms ⊆ parent.perms. 79 let parent_perms_no_meta: i64 = parent.perms & 0xFF 80 let new_perms_no_meta: i64 = new_perms & 0xFF 81 if (new_perms_no_meta & (~parent_perms_no_meta)) != 0 { 82 return 0 as *MemCap 83 } 84 85 // Construct child. Tag bit + meta bits inherit from parent. 86 let child_raw: *u8 = sys_mmap(MEMCAP_BYTES) 87 let child: *MemCap = child_raw as *MemCap 88 child.addr = addr 89 child.base = addr 90 child.length = len 91 // Preserve VALID_TAG (and any other meta bits) from parent; 92 // narrow only the data perms. 93 let meta_bits: i64 = parent.perms & (~0xFF) 94 child.perms = new_perms_no_meta | meta_bits 95 return child 96} 97 98// Narrow an existing cap's permissions in-place by intersecting 99// with a permission-mask. Returns the new (potentially weaker) 100// perms field. NEVER widens. 101func nx_caps_narrow_perms(c: *MemCap, mask: i64) -> i64 { 102 let cur_data: i64 = c.perms & 0xFF 103 let cur_meta: i64 = c.perms & (~0xFF) 104 let new_data: i64 = cur_data & (mask & 0xFF) 105 c.perms = new_data | cur_meta 106 return c.perms 107} 108 109// Revoke: clear the VALID_TAG bit so subsequent derefs fail 110// memcap_valid(). One-way operation. 111func nx_caps_revoke(c: *MemCap) -> i64 { 112 c.perms = c.perms & (~MCAP_VALID_TAG) 113 return 0 114} 115 116// ---- sealer / unsealer pattern (Miller 2006) --------------------- 117// 118// A "sealed" cap has its perms field encrypted with a key. Only 119// holders of the matching unsealer key can re-derive the underlying 120// authority. This is the foundation of typed-channel IPC: the 121// sender seals a payload-cap with the channel's key; the receiver 122// unseals with the matching unsealer. 123// 124// v0.0.1: trivial XOR with the key; not cryptographic. When ChaCha 125// or AES land in our crypto stack, swap for AEAD-sealed caps. 126 127const NX_CAPS_SEAL_BIT: i64 = 0x200 128 129func nx_caps_seal(c: *MemCap, key: i64) -> i64 { 130 // Idempotent: don't re-seal an already-sealed cap. 131 if (c.perms & NX_CAPS_SEAL_BIT) != 0 { return -1 } 132 c.perms = c.perms ^ key 133 c.perms = c.perms | NX_CAPS_SEAL_BIT 134 return 0 135} 136 137func nx_caps_unseal(c: *MemCap, key: i64) -> i64 { 138 if (c.perms & NX_CAPS_SEAL_BIT) == 0 { return -1 } 139 c.perms = c.perms & (~NX_CAPS_SEAL_BIT) 140 c.perms = c.perms ^ key 141 return 0 142} 143 144// Detect sealed state without unsealing. 145func nx_caps_is_sealed(c: *MemCap) -> i64 { 146 if (c.perms & NX_CAPS_SEAL_BIT) != 0 { return 1 } 147 return 0 148} 149 150// ---- self-test ---------------------------------------------------- 151 152func main() -> i64 { 153 // Build a "root" cap covering 0x10000..0x10100 with RW perms. 154 let root_raw: *u8 = sys_mmap(MEMCAP_BYTES) 155 let root: *MemCap = root_raw as *MemCap 156 root.addr = 0x10000 157 root.base = 0x10000 158 root.length = 256 159 root.perms = MCAP_READ | MCAP_WRITE | MCAP_VALID_TAG 160 161 // Derive a read-only subrange [0x10010, 0x10030). 162 let ro_sub: *MemCap = nx_caps_derive_subrange(root, 0x10010, 32, MCAP_READ) 163 if ro_sub == (0 as *MemCap) { return __syscall(93, 10, 0, 0, 0, 0, 0) } 164 if ro_sub.base != 0x10010 { return __syscall(93, 11, 0, 0, 0, 0, 0) } 165 if ro_sub.length != 32 { return __syscall(93, 12, 0, 0, 0, 0, 0) } 166 if (ro_sub.perms & MCAP_READ) == 0 { return __syscall(93, 13, 0, 0, 0, 0, 0) } 167 if (ro_sub.perms & MCAP_WRITE) != 0 { return __syscall(93, 14, 0, 0, 0, 0, 0) } 168 if (ro_sub.perms & MCAP_VALID_TAG) == 0 { return __syscall(93, 15, 0, 0, 0, 0, 0) } 169 170 // Derive a cap OUTSIDE the parent's range -- rejected. 171 let out_of_range: *MemCap = nx_caps_derive_subrange(root, 0x9000, 32, MCAP_READ) 172 if out_of_range != (0 as *MemCap) { return __syscall(93, 20, 0, 0, 0, 0, 0) } 173 174 // Derive with WIDER perms than parent -- rejected (parent has no 175 // EXEC, child can't get EXEC from nowhere). 176 let widen_attempt: *MemCap = nx_caps_derive_subrange(root, 0x10010, 32, 177 MCAP_READ | MCAP_EXEC) 178 if widen_attempt != (0 as *MemCap) { return __syscall(93, 21, 0, 0, 0, 0, 0) } 179 180 // narrow_perms: drop write from a read-write cap. 181 let rw_raw: *u8 = sys_mmap(MEMCAP_BYTES) 182 let rw: *MemCap = rw_raw as *MemCap 183 rw.perms = MCAP_READ | MCAP_WRITE | MCAP_VALID_TAG 184 nx_caps_narrow_perms(rw, MCAP_READ) 185 if (rw.perms & MCAP_READ) == 0 { return __syscall(93, 30, 0, 0, 0, 0, 0) } 186 if (rw.perms & MCAP_WRITE) != 0 { return __syscall(93, 31, 0, 0, 0, 0, 0) } 187 if (rw.perms & MCAP_VALID_TAG) == 0 { return __syscall(93, 32, 0, 0, 0, 0, 0) } 188 189 // revoke: VALID_TAG clears. 190 nx_caps_revoke(ro_sub) 191 if (ro_sub.perms & MCAP_VALID_TAG) != 0 { return __syscall(93, 40, 0, 0, 0, 0, 0) } 192 193 // seal / unseal round-trip. 194 let seal_raw: *u8 = sys_mmap(MEMCAP_BYTES) 195 let s: *MemCap = seal_raw as *MemCap 196 s.perms = MCAP_READ | MCAP_VALID_TAG 197 let key: i64 = 0xCAFEBABE 198 let original_perms: i64 = s.perms 199 nx_caps_seal(s, key) 200 if nx_caps_is_sealed(s) != 1 { return __syscall(93, 50, 0, 0, 0, 0, 0) } 201 if s.perms == original_perms { return __syscall(93, 51, 0, 0, 0, 0, 0) } 202 203 // Re-seal rejected (idempotency). 204 let re_seal: i64 = nx_caps_seal(s, key) 205 if re_seal != -1 { return __syscall(93, 52, 0, 0, 0, 0, 0) } 206 207 // Unseal restores original perms. 208 nx_caps_unseal(s, key) 209 if nx_caps_is_sealed(s) != 0 { return __syscall(93, 53, 0, 0, 0, 0, 0) } 210 if s.perms != original_perms { return __syscall(93, 54, 0, 0, 0, 0, 0) } 211 212 // Unseal-while-not-sealed rejected. 213 let bad_unseal: i64 = nx_caps_unseal(s, key) 214 if bad_unseal != -1 { return __syscall(93, 55, 0, 0, 0, 0, 0) } 215 216 return 0 217}