nx_tea_pinned_gate.nx source

1// nx_tea_pinned_gate.nx -- proves fixed-arg (pinned) execution: a GREEN row's 4th field pins argv and IGNORES the 2// caller's args (so exposing a multi-sub control binary can't be escalated to another sub), while a row WITHOUT a 3// 4th field still uses the caller's args (backward compat). Uses the argecho witness (echoes its argv). PREREQ: 4// _offc/nx_tool_argecho.elf. license_tier: ORIGINAL expect_exit: 0 5import "nx_tool_exec_allow.nx" // tea_resolve_pinned_from / tea_tokenize / tea_run_pinned_from + tr_contains (transitive) 6import "nx_gate.nx" 7 8func pg_write(path: *u8, content: *u8) -> i64 { 9 let fd: i64 = __syscall(257, 0 - 100, path, 0x241, 0x1a4, 0, 0) 10 if fd < 0 { return 0 - 1 } 11 var n: i64 = 0; while content[n] != (0 as u8) { n = n + 1 } 12 sys_write(fd, content, n); sys_close(fd) 13 return 0 14} 15func pg_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 pg_expect(cond: i64, pass: *i64, tot: *i64, label: *u8) -> i64 { 17 tot[0] = tot[0] + 1 18 if cond == 1 { pass[0] = pass[0] + 1; gw(" [PASS] " as *u8) } else { gw(" [FAIL] " as *u8) } 19 gw(label); gw("\n" as *u8) 20 return 0 21} 22 23func main() -> i64 { 24 gw("=== nx_tea_pinned_gate: fixed-arg execution -- pinned row IGNORES caller args (no sub-escalation) ===\n" as *u8) 25 let pbox: *i64 = sys_mmap(16) as *i64; pbox[0] = 0 26 let tbox: *i64 = sys_mmap(16) as *i64; tbox[0] = 0 27 pg_write("/tmp/pg_allow.conf" as *u8, "nx_status\t_offc/nx_tool_argecho.elf\tGREEN\tstatus check\nplain\t_offc/nx_tool_argecho.elf\tGREEN\n" as *u8) 28 29 // T1: resolve a pinned row -> path + haspin=1 + pin bytes 30 let path: *u8 = sys_mmap(4096); let pin: *u8 = sys_mmap(4096); let hp: *i64 = sys_mmap(16) as *i64 31 let c1: i64 = tea_resolve_pinned_from("/tmp/pg_allow.conf" as *u8, "nx_status" as *u8, 9, path, 4096, pin, 4096, hp) 32 var t1: i64 = 0 33 if c1 == TEA_OK { if hp[0] == 1 { if pg_streq(pin, "status check" as *u8) == 1 { t1 = 1 } } } 34 pg_expect(t1, pbox, tbox, "T1 pinned row resolves: path + haspin=1 + pin='status check'" as *u8) 35 36 // T2: tokenize 37 let av: *i64 = sys_mmap(512) as *i64; let sc: *u8 = sys_mmap(512) 38 let nt: i64 = tea_tokenize("alpha beta gamma" as *u8, av, 0, sc, 512) 39 var t2: i64 = 0 40 if nt == 3 { if pg_streq(av[0] as *u8, "alpha" as *u8) == 1 { if pg_streq(av[2] as *u8, "gamma" as *u8) == 1 { t2 = 1 } } } 41 pg_expect(t2, pbox, tbox, "T2 tokenize 'alpha beta gamma' -> 3 tokens" as *u8) 42 43 let out: *u8 = sys_mmap(65536); let olen: *i64 = sys_mmap(16) as *i64; let rc: *i64 = sys_mmap(16) as *i64 44 45 // T3 SECURITY: a pinned tool run with a HOSTILE caller arg -> executes the PINNED args, NOT the caller's 46 let cav: *i64 = sys_mmap(512) as *i64; cav[1] = "HACKERINJECT" as *u8 as i64; cav[2] = 0 47 tea_run_pinned_from("/tmp/pg_allow.conf" as *u8, "nx_status" as *u8, 9, cav, out, 65536, olen, rc) 48 var t3: i64 = 0 49 if tr_contains(out, olen[0], "status" as *u8) == 1 { if tr_contains(out, olen[0], "check" as *u8) == 1 { if tr_contains(out, olen[0], "HACKERINJECT" as *u8) == 0 { t3 = 1 } } } 50 pg_expect(t3, pbox, tbox, "T3 SECURITY: pinned run ignores caller arg -> echoes 'status check', NOT 'HACKERINJECT'" as *u8) 51 52 // T4 backward-compat: a NON-pinned row uses the caller's args 53 let cav2: *i64 = sys_mmap(512) as *i64; cav2[1] = "CALLERVAL" as *u8 as i64; cav2[2] = 0 54 tea_run_pinned_from("/tmp/pg_allow.conf" as *u8, "plain" as *u8, 5, cav2, out, 65536, olen, rc) 55 var t4: i64 = 0 56 if tr_contains(out, olen[0], "CALLERVAL" as *u8) == 1 { t4 = 1 } 57 pg_expect(t4, pbox, tbox, "T4 back-compat: non-pinned row uses caller arg (echoes 'CALLERVAL')" as *u8) 58 59 gw("\n=== nx_tea_pinned_gate " as *u8); gn(pbox[0]); gw("/" as *u8); gn(tbox[0]); gw(" ===\n" as *u8) 60 if pbox[0] == tbox[0] { gw("TEA-PINNED GREEN -- fixed-arg pins the subcommand; caller can never escalate the argv\n" as *u8); sys_exit(0); return 0 } 61 gw("TEA-PINNED RED\n" as *u8); sys_exit(1); return 1 62}