nx_tool_exec_allow_gate.nx source
↩ module page · 98 lines · 5962 B
1// nx_tool_exec_allow_gate.nx -- GATE for R1 (nx_tool_exec_allow), composing R0 (nx_tool_run). Proves the
2// execution allowlist is fail-closed and never-brick: only an allowlisted, gate-GREEN row resolves to an ELF
3// path and runs; a non-GREEN row is present-but-blocked; an unknown name and a traversal name ("../x") both
4// refuse; and a GREEN row actually EXECUTES its ELF and captures real stdout. Target = the canonical no-op
5// nx_tool_ping (a SEPARATE tiny ELF, zero recursion risk). Writes its allowlist to /tmp (never touches a
6// real config). PREREQ: build nx_tool_ping FIRST (produces _offc/nx_tool_ping.elf).
7// license_tier: ORIGINAL expect_exit: 0
8import "nx_tool_exec_allow.nx"
9import "nx_gate_verdict.nx"
10
11const TEA_TESTCONF: *u8 = "/tmp/nx_tea_test.conf" as *u8
12
13func ew(s: *u8) -> i64 { var n: i64=0; while s[n]!=(0 as u8){n=n+1} sys_write(1,s,n); return 0 }
14func en(v: i64) -> i64 { let bb: *u8=sys_mmap(28); var m: i64=v; if m<0{sys_write(1,"-" as *u8,1);m=0-m} let t: *u8=sys_mmap(28); var k: i64=0; if m==0{t[0]=48 as u8;k=1} while m>0{t[k]=(48+(m%10)) as u8;m=m/10;k=k+1} var i: i64=0; while i<k{bb[i]=t[k-1-i];i=i+1} sys_write(1,bb,k); return 0 }
15func e_streq(a: *u8, b: *u8) -> i64 { var i: i64=0; while a[i]!=(0 as u8){ if a[i]!=b[i]{return 0} i=i+1 } if b[i]!=(0 as u8){return 0} return 1 }
16func e_slen(s: *u8) -> i64 { var n: i64=0; while s[n]!=(0 as u8){n=n+1} return n }
17
18// write the test allowlist (O_WRONLY|O_CREAT|O_TRUNC=0x241, mode 0644) via openat(AT_FDCWD=-100)
19func tea_write_testconf() -> i64 {
20 let fd: i64 = __syscall(257, 0 - 100, TEA_TESTCONF, 0x241, 0x1a4, 0, 0)
21 if fd < 0 { return 0 - 1 }
22 let body: *u8 = "# nx execution allowlist (test)\nselftest\t_offc/nx_tool_ping.elf\tGREEN\nblocked\t_offc/nx_tool_ping.elf\tRED\n" as *u8
23 sys_write(fd, body, e_slen(body))
24 sys_close(fd)
25 return 0
26}
27
28func main() -> i64 {
29 ew("=== nx_tool_exec_allow_gate (R1: execution allowlist, fail-closed + never-brick, composing R0) ===\n" as *u8)
30 if tea_write_testconf() != 0 { ew("FAIL: could not write test allowlist\n" as *u8); sys_exit(1); return 1 }
31
32 var pass: i64 = 0
33 var tot: i64 = 0
34 let path: *u8 = sys_mmap(4096)
35
36 // T1: GREEN row resolves to its ELF path
37 tot = tot + 1
38 let r1: i64 = tea_resolve_from(TEA_TESTCONF, "selftest" as *u8, 8, path, 4096)
39 var ok1: i64 = 1
40 if r1 != TEA_OK { ok1 = 0 }
41 if e_streq(path, "_offc/nx_tool_ping.elf" as *u8) == 0 { ok1 = 0 }
42 if ok1 == 1 { pass = pass + 1; ew("PASS T1 GREEN row -> TEA_OK, path=_offc/nx_tool_ping.elf\n" as *u8) } else { ew("FAIL T1 rc=" as *u8); en(r1); ew(" path=" as *u8); ew(path); ew("\n" as *u8) }
43
44 // T2 NEG: non-GREEN row -> BLOCKED, empty path (listed but NOT runnable)
45 tot = tot + 1
46 path[0] = 0 as u8
47 let r2: i64 = tea_resolve_from(TEA_TESTCONF, "blocked" as *u8, 7, path, 4096)
48 var ok2: i64 = 1
49 if r2 != TEA_BLOCKED { ok2 = 0 }
50 if path[0] != (0 as u8) { ok2 = 0 }
51 if ok2 == 1 { pass = pass + 1; ew("PASS T2 non-GREEN row -> BLOCKED, empty path (present != runnable)\n" as *u8) } else { ew("FAIL T2 rc=" as *u8); en(r2); ew("\n" as *u8) }
52
53 // T3 NEG: unknown name -> NOTFOUND
54 tot = tot + 1
55 let r3: i64 = tea_resolve_from(TEA_TESTCONF, "ghost" as *u8, 5, path, 4096)
56 if r3 == TEA_NOTFOUND { pass = pass + 1; ew("PASS T3 unknown name -> NOTFOUND\n" as *u8) } else { ew("FAIL T3 rc=" as *u8); en(r3); ew("\n" as *u8) }
57
58 // T4 NEG (never-brick): a traversal name is refused by tea_name_ok BEFORE it can index anything
59 tot = tot + 1
60 let r4: i64 = tea_resolve_from(TEA_TESTCONF, "../etc/passwd" as *u8, 13, path, 4096)
61 var ok4: i64 = 1
62 if r4 != TEA_NOTFOUND { ok4 = 0 }
63 if path[0] != (0 as u8) { ok4 = 0 }
64 if ok4 == 1 { pass = pass + 1; ew("PASS T4 never-brick: traversal name '../etc/passwd' refused (no '/' reaches resolve)\n" as *u8) } else { ew("FAIL T4 rc=" as *u8); en(r4); ew("\n" as *u8) }
65
66 // T5: composed R0+R1 -- resolve the GREEN row AND execute it (no arg), capturing real stdout + exit code
67 tot = tot + 1
68 let out: *u8 = sys_mmap(65536)
69 let lenp: *i64 = sys_mmap(16) as *i64
70 let rcp: *i64 = sys_mmap(16) as *i64
71 let ec: i64 = tea_run_from(TEA_TESTCONF, "selftest" as *u8, 8, 0 as *u8, out, 65536, lenp, rcp)
72 var ok5: i64 = 1
73 if rcp[0] != TEA_OK { ok5 = 0 }
74 if ec != 0 { ok5 = 0 }
75 if tr_contains(out, lenp[0], "NX_TOOL_PING_OK" as *u8) != 1 { ok5 = 0 }
76 if ok5 == 1 { pass = pass + 1; ew("PASS T5 composed exec: allowlisted GREEN tool ran, exit=" as *u8); en(ec); ew(" captured " as *u8); en(lenp[0]); ew(" bytes incl sentinel\n" as *u8) }
77 else { ew("FAIL T5 rc=" as *u8); en(rcp[0]); ew(" exit=" as *u8); en(ec); ew(" len=" as *u8); en(lenp[0]); ew("\n" as *u8) }
78
79 // T6 NEG: tea_run on a BLOCKED tool must NOT execute -- returns the refusal code, zero capture
80 tot = tot + 1
81 lenp[0] = 0
82 let ec6: i64 = tea_run_from(TEA_TESTCONF, "blocked" as *u8, 7, 0 as *u8, out, 65536, lenp, rcp)
83 var ok6: i64 = 1
84 if ec6 != TEA_BLOCKED { ok6 = 0 }
85 if lenp[0] != 0 { ok6 = 0 }
86 if ok6 == 1 { pass = pass + 1; ew("PASS T6 blocked tool NOT executed -> refusal code, zero capture\n" as *u8) } else { ew("FAIL T6 ec=" as *u8); en(ec6); ew(" len=" as *u8); en(lenp[0]); ew("\n" as *u8) }
87
88 ew("nx_tool_exec_allow_gate pass=" as *u8); en(pass); ew("/" as *u8); en(tot)
89 // MIGRATED onto nx_gate_verdict by nx_gate_dry_apply (D001, minimal form): every check
90 // row above is untouched, so the PASS/FAIL vector cannot change; only the hand-rolled
91 // verdict emission is replaced by the ONE shared base class. Proven by nx_gate_migrate verify.
92 let ctr__dry: *i64 = gv_ctr()
93 ctr__dry[0] = pass
94 ctr__dry[1] = tot
95 let rc__dry: i64 = gv_verdict("TOOL-EXEC-ALLOW-GATE" as *u8, ctr__dry, "only vetted GREEN organs run; never-brick + fail-closed proven; R2 can wire /mcp tools/call)" as *u8)
96 sys_exit(rc__dry)
97 return rc__dry
98}