nx_memcap.nx source
↩ module page · 274 lines · 9812 B
1// memcap.nx -- CHERI-style memory capabilities, pure software.
2//
3// Pointer-with-bounds-and-permissions, implemented entirely in
4// software. When Nishi silicon ships with hardware capabilities
5// (CHERI-RISC-V extension, or our own), the compiler recognises
6// MemCap<T> and emits single-instruction capability ops; the
7// software runtime becomes a no-op or is replaced by the hardware
8// path. Same NishiLang source, silicon-accelerated backend.
9//
10// This is the 40-year bet: build invariants in software now, keep
11// the HW/SW interface stable, upgrade silicon when we can fab it.
12//
13// Distinct from runtime/cap.nx: that file covers ACCESS
14// capabilities (who can call fs_open), which are coarse-grained
15// and language-level. This file covers MEMORY capabilities (what
16// bytes a pointer can touch), which are fine-grained and per-
17// allocation. Both systems plug into the Nishi silicon story:
18// access caps become compartment IDs, memory caps become CHERI
19// pointer tags.
20//
21// Reference papers / systems:
22// Watson et al 2015 "CHERI: A Hybrid Capability-System
23// Architecture for Scalable Software Compartmentalization"
24// Woodruff et al 2014 "The CHERI capability model"
25// Nienhuis et al 2020 "Rigorous engineering for hardware security"
26// Arm Morello -- production CHERI-Armv8 (2022)
27// RISC-V CHERI extension -- ratified draft (2024)
28//
29// Layout (32 bytes in software):
30// + 0 .. + 7 : address (i64, the actual pointer)
31// + 8 .. + 15 : base (i64, lower bound inclusive)
32// + 16 .. + 23 : length (i64, bytes from base)
33// + 24 .. + 31 : perms + tag (packed i64)
34// bit 0 : READ (load permitted)
35// bit 1 : WRITE (store permitted)
36// bit 2 : EXEC (jump permitted -- future)
37// bit 3 : CAP_LOAD (can load a capability through)
38// bit 4 : CAP_STORE (can store a capability through)
39// bit 5 : SEAL (non-deref, unforgeable handle)
40// bit 8 : VALID_TAG (mandatory; cleared on raw memcpy)
41// bits 9..63 : generation (monotonic, detects UAF)
42//
43// Silicon target: 128-bit compressed capability with hardware-
44// tagged memory. Same semantic, 4x smaller + bounds enforcement
45// free at runtime.
46
47// nx_safety_envelope:
48// intended_use: AUTO_APPLIED -- primitive-specific tuning queued
49// sil_target: SIL1
50// evidence: [bulk_applied_2026-05-16, see-file-comment-for-detail]
51// verdict: NOT_YET_EVALUATED
52
53import "nx_syscalls.nx"
54import "nx_assert.nx"
55const MCAP_MAGIC_10000: i64 = 10000
56
57// --- permission bits ------------------------------------------------
58
59const MCAP_READ: i64 = 0x001
60const MCAP_WRITE: i64 = 0x002
61const MCAP_EXEC: i64 = 0x004
62const MCAP_CAP_LOAD: i64 = 0x008
63const MCAP_CAP_STORE: i64 = 0x010
64const MCAP_SEAL: i64 = 0x020
65const MCAP_VALID_TAG: i64 = 0x100
66
67// Common combinations.
68const MCAP_RW: i64 = 0x103 // READ | WRITE | VALID_TAG
69const MCAP_RO: i64 = 0x101 // READ | VALID_TAG
70
71// --- struct ---------------------------------------------------------
72
73struct MemCap {
74 addr: i64,
75 base: i64,
76 length: i64,
77 perms: i64,
78}
79
80const MEMCAP_BYTES: i64 = 32
81
82// --- construction ---------------------------------------------------
83
84// Create a fresh rw-capable capability over [base, base+length).
85func memcap_new(addr: i64, base: i64, length: i64, perms: i64) -> *MemCap {
86 let c_raw: *u8 = sys_mmap(MEMCAP_BYTES)
87 let c: *MemCap = c_raw as *MemCap
88 c.addr = addr
89 c.base = base
90 c.length = length
91 c.perms = perms | MCAP_VALID_TAG
92 return c
93}
94
95// Allocate `size` bytes + return a capability covering it. The
96// standard replacement for `sys_mmap(size) as *T`.
97func memcap_alloc(size: i64) -> *MemCap {
98 let mem: *u8 = sys_mmap(size)
99 return memcap_new(mem as i64, mem as i64, size, MCAP_RW)
100}
101
102// --- checks ---------------------------------------------------------
103
104// Is this capability usable for ANY operation?
105func memcap_valid(c: *MemCap) -> i64 {
106 if c == (0 as *MemCap) { return 0 }
107 if (c.perms & MCAP_VALID_TAG) == 0 { return 0 }
108 return 1
109}
110
111// Can read n bytes starting at addr+offset?
112func memcap_can_read(c: *MemCap, offset: i64, n: i64) -> i64 {
113 if memcap_valid(c) == 0 { return 0 }
114 if (c.perms & MCAP_READ) == 0 { return 0 }
115 let pos: i64 = c.addr + offset
116 if pos < c.base { return 0 }
117 if pos + n > c.base + c.length { return 0 }
118 return 1
119}
120
121// Same for write.
122func memcap_can_write(c: *MemCap, offset: i64, n: i64) -> i64 {
123 if memcap_valid(c) == 0 { return 0 }
124 if (c.perms & MCAP_WRITE) == 0 { return 0 }
125 let pos: i64 = c.addr + offset
126 if pos < c.base { return 0 }
127 if pos + n > c.base + c.length { return 0 }
128 return 1
129}
130
131// --- load/store operations -----------------------------------------
132
133// Checked i64 load. Asserts on violation.
134func memcap_load_i64(c: *MemCap, offset: i64) -> i64 {
135 nx_assert(memcap_can_read(c, offset, 8),
136 "memcap_load_i64: bounds/perm check failed" as *u8)
137 let p: *i64 = (c.addr + offset) as *i64
138 return *p
139}
140
141// Checked i64 store. Asserts on violation.
142func memcap_store_i64(c: *MemCap, offset: i64, val: i64) -> i64 {
143 nx_assert(memcap_can_write(c, offset, 8),
144 "memcap_store_i64: bounds/perm check failed" as *u8)
145 let p: *i64 = (c.addr + offset) as *i64
146 *p = val
147 return 0
148}
149
150// Checked u8 load (1 byte).
151func memcap_load_u8(c: *MemCap, offset: i64) -> i64 {
152 nx_assert(memcap_can_read(c, offset, 1),
153 "memcap_load_u8: bounds/perm check failed" as *u8)
154 let p: *u8 = (c.addr + offset) as *u8
155 return p[0]
156}
157
158// Checked u8 store.
159func memcap_store_u8(c: *MemCap, offset: i64, val: i64) -> i64 {
160 nx_assert(memcap_can_write(c, offset, 1),
161 "memcap_store_u8: bounds/perm check failed" as *u8)
162 let p: *u8 = (c.addr + offset) as *u8
163 p[0] = val
164 return 0
165}
166
167// --- derivation (monotonic) -----------------------------------------
168//
169// The fundamental CHERI invariant: a derived capability can ONLY
170// narrow the parent, never widen. Enforced in silicon via tagged
171// memory; enforced here by asserts.
172
173// Narrow bounds: derive a cap over a subrange of parent.
174func memcap_subrange(parent: *MemCap, sub_offset: i64, sub_len: i64) -> *MemCap {
175 nx_assert(memcap_valid(parent), "memcap_subrange: parent not valid" as *u8)
176 let new_base: i64 = parent.addr + sub_offset
177 if new_base < parent.base {
178 nx_assert(0, "memcap_subrange: underflow" as *u8)
179 }
180 if new_base + sub_len > parent.base + parent.length {
181 nx_assert(0, "memcap_subrange: overflow" as *u8)
182 }
183 return memcap_new(new_base, new_base, sub_len, parent.perms)
184}
185
186// Narrow perms: drop bits. Can only remove permissions the parent
187// already has; cannot grant new permissions.
188func memcap_restrict(c: *MemCap, new_perms: i64) -> *MemCap {
189 nx_assert(memcap_valid(c), "memcap_restrict: c not valid" as *u8)
190 if (new_perms & c.perms) != new_perms {
191 nx_assert(0, "memcap_restrict: cannot widen perms" as *u8)
192 }
193 return memcap_new(c.addr, c.base, c.length, new_perms | MCAP_VALID_TAG)
194}
195
196// Seal: derive a non-dereferenceable handle. Holder can pass it
197// around but cannot follow it. Analogous to CHERI 'cseal'.
198func memcap_seal(c: *MemCap) -> *MemCap {
199 nx_assert(memcap_valid(c), "memcap_seal: c not valid" as *u8)
200 return memcap_new(c.addr, c.base, c.length,
201 (c.perms | MCAP_SEAL) | MCAP_VALID_TAG)
202}
203
204// --- self-test ------------------------------------------------------
205
206func main() -> i64 {
207 // 1: construction + valid tag
208 let c: *MemCap = memcap_alloc(64)
209 if memcap_valid(c) != 1 { return __syscall(93, 10, 0, 0, 0, 0, 0) }
210 if c.length != 64 { return __syscall(93, 11, 0, 0, 0, 0, 0) }
211
212 // 2: load/store round-trip
213 memcap_store_i64(c, 0, 42)
214 memcap_store_i64(c, 8, 100)
215 if memcap_load_i64(c, 0) != 42 {
216 return __syscall(93, 20, 0, 0, 0, 0, 0)
217 }
218 if memcap_load_i64(c, 8) != 100 {
219 return __syscall(93, 21, 0, 0, 0, 0, 0)
220 }
221
222 // 3: bounds check positive
223 if memcap_can_read(c, 56, 8) != 1 {
224 return __syscall(93, 30, 0, 0, 0, 0, 0)
225 }
226 // 4: bounds check negative (1 byte past end)
227 if memcap_can_read(c, 57, 8) != 0 {
228 return __syscall(93, 40, 0, 0, 0, 0, 0)
229 }
230 // 5: far out of range
231 if memcap_can_write(c, MCAP_MAGIC_10000, 8) != 0 {
232 return __syscall(93, 50, 0, 0, 0, 0, 0)
233 }
234
235 // 6: subrange narrows bounds
236 let sub: *MemCap = memcap_subrange(c, 16, 32)
237 memcap_store_i64(sub, 0, 7)
238 // Parent sees the write at offset 16 (= sub's offset 0)
239 if memcap_load_i64(c, 16) != 7 {
240 return __syscall(93, 60, 0, 0, 0, 0, 0)
241 }
242 // Sub can't reach beyond its length
243 if memcap_can_read(sub, 32, 1) != 0 {
244 return __syscall(93, 61, 0, 0, 0, 0, 0)
245 }
246
247 // 7: restrict drops perms monotonically
248 let ro: *MemCap = memcap_restrict(c, MCAP_READ | MCAP_VALID_TAG)
249 if memcap_can_read(ro, 0, 8) != 1 {
250 return __syscall(93, 70, 0, 0, 0, 0, 0)
251 }
252 if memcap_can_write(ro, 0, 8) != 0 {
253 return __syscall(93, 71, 0, 0, 0, 0, 0)
254 }
255
256 // 8: seal sets the seal bit
257 let sealed: *MemCap = memcap_seal(c)
258 if (sealed.perms & MCAP_SEAL) == 0 {
259 return __syscall(93, 80, 0, 0, 0, 0, 0)
260 }
261
262 // 9: null cap not valid
263 if memcap_valid(0 as *MemCap) != 0 {
264 return __syscall(93, 90, 0, 0, 0, 0, 0)
265 }
266
267 // 10: u8 load/store round-trip (byte-level ops)
268 memcap_store_u8(c, 24, 0xA5)
269 if memcap_load_u8(c, 24) != 0xA5 {
270 return __syscall(93, 100, 0, 0, 0, 0, 0)
271 }
272
273 return 0
274}