nx_spatial_probe.nx source
↩ module page · 57 lines · 2537 B
1// nx_spatial_probe.nx -- STANDING WITNESS for the spatial-safety gap (CWE-787/125).
2// Measures, does not assert. Three cells, each printed with its OWN control:
3// CELL A: [N]T indexed by a COMPILE-TIME CONSTANT -- already compile-time checked (a negative
4// control lives in nx_spatial_negctl_const.nx: it must FAIL TO COMPILE).
5// CELL B: [N]T indexed by a RUNTIME VARIABLE -- the GAP under test.
6// CELL C: *T (raw pointer) indexed out of range -- no length is carried; C-class by construction.
7// A cell prints UNCHECKED when the out-of-range access completed and the program kept running.
8// When the bounds-check rung lands, cell B must instead ABORT -- which this probe cannot print,
9// so the gate asserts on the EXIT CODE, not on this text.
10import "nx_fmt.nx"
11
12func main() -> i64 {
13 fmt_puts("=== nx_spatial_probe -- measured spatial-safety status ===\n" as *u8)
14
15 // ---------------- CELL B: fixed array, RUNTIME index ----------------
16 // buf is [4]i64. `guard` is a neighbouring local the OOB write is expected to land on or near;
17 // it is read back afterwards so the corruption is OBSERVABLE rather than inferred.
18 var guard: i64 = 555
19 var buf: [4]i64
20 var i: i64 = 0
21 while i < 4 {
22 buf[i] = 100 + i
23 i = i + 1
24 }
25 // In-range control first: proves the indexing path itself works before we push it out of range.
26 var ok: i64 = 2
27 let inrange: i64 = buf[ok]
28 fmt_puts(" cellB control in-range buf[2]="); fmt_putn(inrange); fmt_puts(" (expect 102)\n" as *u8)
29
30 // The GAP: index 6 on a 4-element array, via a runtime variable the compiler must not fold.
31 var j: i64 = 4
32 j = j + 2
33 let oob_read: i64 = buf[j]
34 fmt_puts(" cellB VARIABLE-index OOB READ buf[6] completed, value=" as *u8)
35 fmt_putn(oob_read)
36 fmt_puts(" => UNCHECKED\n" as *u8)
37
38 // ---------------- CELL C: raw pointer, no length ----------------
39 let p: *i64 = sys_mmap(16) as *i64
40 p[0] = 11
41 p[1] = 22
42 var m: i64 = 1
43 m = m + 1
44 p[m] = 33
45 let oob_ptr: i64 = p[m]
46 fmt_puts(" cellC POINTER OOB WRITE+READ p[2]=" as *u8)
47 fmt_putn(oob_ptr)
48 fmt_puts(" => UNCHECKED (no length carried by *T)\n" as *u8)
49
50 fmt_puts(" cellB guard local after OOB guard=" as *u8)
51 fmt_putn(guard)
52 fmt_puts("\n" as *u8)
53
54 fmt_puts("VERDICT: reaching this line at all means the RUNTIME-index array access was NOT bounds-checked.\n" as *u8)
55 fmt_puts("NX-SPATIAL-PROBE UNCHECKED exit=7\n" as *u8)
56 return 7
57}