code wiki / (root) / nx_opennet_posture_gate.nx

nx_opennet_posture_gate.nx source

↩ module page · 77 lines · 3677 B

1// nx_opennet_posture_gate.nx -- liar-killed GATE for the open-net posture ruler (S15/O2). 2// Proves the security invariant DISCRIMINATES: unauth-deny surfaces PASS only on 401/403, a DENY 3// surface that serves 200 is caught as a LEAK (not a silent pass -- the load-bearing negative 4// control), public surfaces PASS only on 200, redirects on 301/302, an unreachable/parse-fail is 5// UNREACH (never a fabricated PASS), the HTTP-status parser handles real response lines + rejects 6// non-HTTP, and the sovereign-edge header check detects our stamp + rejects its absence. Exit 0 7// only on all-PASS. 8// license_tier: ORIGINAL expect_exit: 0 9import "nx_syscalls.nx" 10import "nx_opennet_posture_core.nx" 11 12func p_puts(s: *u8) -> i64 { var n: i64 = 0; while s[n] != (0 as u8) { n = n + 1 } sys_write(1, s, n); return 0 } 13 14func p_putn(v: i64) -> i64 { 15 let b: *u8 = sys_mmap(32) 16 let e: i64 = ccz_cat_num(b, 0, v) 17 sys_write(1, b, e) 18 return 0 19} 20 21func p_check(name: *u8, got: i64, want: i64, passp: *i64) -> i64 { 22 p_puts("T " as *u8) 23 p_puts(name) 24 p_puts(" got=" as *u8) 25 p_putn(got) 26 p_puts(" want=" as *u8) 27 p_putn(want) 28 if got == want { p_puts(" PASS\n" as *u8); passp[0] = passp[0] + 1 } else { p_puts(" FAIL\n" as *u8) } 29 return 0 30} 31 32func main(argc: i64, argv: *i64) -> i64 { 33 let pass: *i64 = sys_mmap(16) as *i64 34 pass[0] = 0 35 36 // --- decision matrix --- 37 p_check("deny-401-PASS" as *u8, op_verdict(401, OP_DENY), OP_PASS, pass) 38 p_check("deny-403-PASS" as *u8, op_verdict(403, OP_DENY), OP_PASS, pass) 39 // THE load-bearing negative control: a deny surface serving 200 to no-cred = LEAK, caught 40 p_check("deny-200-LEAK" as *u8, op_verdict(200, OP_DENY), OP_LEAK, pass) 41 p_check("deny-500-FAIL" as *u8, op_verdict(500, OP_DENY), OP_FAIL, pass) 42 p_check("public-200-PASS" as *u8, op_verdict(200, OP_PUBLIC), OP_PASS, pass) 43 // a public surface that 401s = availability regression, not a pass 44 p_check("public-401-FAIL" as *u8, op_verdict(401, OP_PUBLIC), OP_FAIL, pass) 45 p_check("redirect-301-PASS" as *u8, op_verdict(301, OP_REDIRECT), OP_PASS, pass) 46 p_check("redirect-302-PASS" as *u8, op_verdict(302, OP_REDIRECT), OP_PASS, pass) 47 // unreachable / unparseable -> UNREACH, NEVER a silent PASS 48 p_check("unreach-UNREACH" as *u8, op_verdict(0 - 1, OP_DENY), OP_UNREACH, pass) 49 50 // --- status parser --- 51 let r401: *u8 = "HTTP/1.1 401 Unauthorized\r\nContent-Type: application/json\r\n\r\n{}" as *u8 52 p_check("parse-401" as *u8, op_http_status(r401, 60), 401, pass) 53 let r200: *u8 = "HTTP/1.1 200 OK\r\nX-Served-By: nishi-substrate-v2\r\n\r\nhi" as *u8 54 p_check("parse-200" as *u8, op_http_status(r200, 55), 200, pass) 55 // non-HTTP garbage -> -1 (never a fabricated status) 56 let rjunk: *u8 = "<html>synology login</html>" as *u8 57 p_check("parse-nonhttp-neg" as *u8, op_http_status(rjunk, 27), 0 - 1, pass) 58 59 // --- sovereign-edge header check --- 60 p_check("sovereign-present" as *u8, op_is_sovereign(r200, 55), 1, pass) 61 p_check("sovereign-absent" as *u8, op_is_sovereign(r401, 60), 0, pass) 62 63 // --- expect-keyword mapping --- 64 var okmap: i64 = 1 65 if op_expect_id("deny" as *u8) != OP_DENY { okmap = 0 } 66 if op_expect_id("serve-public" as *u8) != OP_PUBLIC { okmap = 0 } 67 if op_expect_id("redirect" as *u8) != OP_REDIRECT { okmap = 0 } 68 if op_expect_id("bogus" as *u8) != 0 - 1 { okmap = 0 } 69 p_check("expect-keyword-map" as *u8, okmap, 1, pass) 70 71 p_puts("OPP-GATE pass=" as *u8) 72 p_putn(pass[0]) 73 p_puts("/15 verdict=" as *u8) 74 if pass[0] == 15 { p_puts("GREEN\n" as *u8); return 0 } 75 p_puts("RED\n" as *u8) 76 return 1 77}