nx_property_test.nx source
↩ module page · 93 lines · 5129 B
1// nx_property_test.nx -- PROPERTY-BASED + METAMORPHIC testing of the capability core (census gap). Instead of fixed
2// cases, GENERATE random capabilities (reproducible LCG) and assert INVARIANTS hold over hundreds of them:
3// P1 (property): verify(issue(allow,exp), tool) == OK <=> (tool in allow) AND (not expired)
4// M1 (metamorphic): attenuate(all-cap, narrow) grants tool <=> tool in narrow (attenuation never widens)
5// A single violation prints the (minimal-ish) counterexample and reds. This is what would have caught a subtler
6// MAC/allow-logic bug that a hand-written fixed case might miss. license_tier: ORIGINAL
7import "nx_cap_token.nx"
8import "nx_gate.nx"
9
10// reproducible LCG (fixed seed -> same sequence every run; the operator's reproducibility ethos)
11func pt_rand(state: *i64) -> i64 { state[0] = state[0] * 1103515245 + 12345; return (state[0] >> 16) & 0x7fffffff }
12
13// tool name "t<i>" (i in 0..7) into buf; returns len (2).
14func pt_tool(i: i64, buf: *u8) -> i64 { buf[0] = 116 as u8; buf[1] = (48 + i) as u8; return 2 }
15
16// allow-string from an 8-bit mask: comma-joined t<i> for set bits, into buf; returns len (0 if mask==0).
17func pt_allow(mask: i64, buf: *u8) -> i64 {
18 var o: i64 = 0; var i: i64 = 0; var first: i64 = 1
19 while i < 8 {
20 if ((mask >> i) & 1) == 1 {
21 if first == 0 { buf[o] = 44 as u8; o = o + 1 } // ','
22 buf[o] = 116 as u8; o = o + 1; buf[o] = (48 + i) as u8; o = o + 1
23 first = 0
24 }
25 i = i + 1
26 }
27 return o
28}
29
30func main() -> i64 {
31 gw("=== nx_property_test: random-generated capabilities, INVARIANTS must hold (property + metamorphic) ===\n" as *u8)
32 let key: *u8 = "prop-test-key-abcdefghij0123456789" as *u8
33 let klen: i64 = capt_slen(key)
34 let now: i64 = 1782000000
35 let st: *i64 = sys_mmap(16) as *i64; st[0] = 1234567
36 let iters: i64 = 300
37 let tok: *u8 = sys_mmap(1024)
38 let allowb: *u8 = sys_mmap(128)
39 let toolb: *u8 = sys_mmap(16)
40 let narrowb: *u8 = sys_mmap(128)
41 let atok: *u8 = sys_mmap(1024)
42
43 // ---- P1: the core authorization invariant over random (allow-set, expiry, tool) ----
44 var p_viol: i64 = 0; var i: i64 = 0
45 while i < iters {
46 let mask: i64 = pt_rand(st) & 0xff
47 let future: i64 = pt_rand(st) & 1
48 var exp: i64 = 1; if future == 1 { exp = 9999999999 }
49 let ti: i64 = pt_rand(st) & 7
50 let alen: i64 = pt_allow(mask, allowb)
51 let tlen: i64 = pt_tool(ti, toolb)
52 let tn: i64 = capt_issue(key, klen, allowb, alen, exp, i + 1, tok, 1024)
53 var actual: i64 = 0; if capt_verify(key, klen, tok, tn, toolb, tlen, now) == CAPT_OK { actual = 1 }
54 var expected: i64 = 0; if ((mask >> ti) & 1) == 1 { if future == 1 { expected = 1 } }
55 if actual != expected {
56 p_viol = p_viol + 1
57 if p_viol <= 3 { gw(" [P1 VIOLATION] mask=" as *u8); gn(mask); gw(" tool=t" as *u8); gn(ti); gw(" future=" as *u8); gn(future); gw(" expected=" as *u8); gn(expected); gw(" actual=" as *u8); gn(actual); gw("\n" as *u8) }
58 }
59 i = i + 1
60 }
61 gw(" P1 verify == (tool in allow AND not-expired) over " as *u8); gn(iters); gw(" cases: " as *u8)
62 if p_viol == 0 { gw("HOLDS\n" as *u8) } else { gw("VIOLATED " as *u8); gn(p_viol); gw("x\n" as *u8) }
63
64 // ---- M1 (metamorphic): attenuate the ALL-cap to a random subset -> grants a tool iff it is in the subset ----
65 var m_viol: i64 = 0
66 let base: i64 = capt_issue(key, klen, "*" as *u8, 1, 9999999999, 1, tok, 1024) // base grants everything
67 i = 0
68 while i < iters {
69 let nmask: i64 = pt_rand(st) & 0xff
70 let ti: i64 = pt_rand(st) & 7
71 let nlen: i64 = pt_allow(nmask, narrowb)
72 let tlen: i64 = pt_tool(ti, toolb)
73 if nlen > 0 {
74 let an: i64 = capt_attenuate(key, klen, tok, base, narrowb, nlen, 9999999999, i + 2, atok, 1024)
75 if an > 0 {
76 var actual: i64 = 0; if capt_verify(key, klen, atok, an, toolb, tlen, now) == CAPT_OK { actual = 1 }
77 var expected: i64 = 0; if ((nmask >> ti) & 1) == 1 { expected = 1 }
78 if actual != expected {
79 m_viol = m_viol + 1
80 if m_viol <= 3 { gw(" [M1 VIOLATION] narrow=" as *u8); gn(nmask); gw(" tool=t" as *u8); gn(ti); gw(" expected=" as *u8); gn(expected); gw(" actual=" as *u8); gn(actual); gw("\n" as *u8) }
81 }
82 }
83 }
84 i = i + 1
85 }
86 gw(" M1 attenuate(*, narrow) grants tool == (tool in narrow) over " as *u8); gn(iters); gw(" cases: " as *u8)
87 if m_viol == 0 { gw("HOLDS\n" as *u8) } else { gw("VIOLATED " as *u8); gn(m_viol); gw("x\n" as *u8) }
88
89 gw("\n=== nx_property_test: P1 viol=" as *u8); gn(p_viol); gw(" M1 viol=" as *u8); gn(m_viol); gw(" ===\n" as *u8)
90 if p_viol == 0 { if m_viol == 0 { gw("PROPERTY GREEN -- the capability invariants hold over 600 generated cases.\n" as *u8); sys_exit(0); return 0 } }
91 gw("PROPERTY RED -- an invariant was VIOLATED (counterexample above); the capability logic has a bug.\n" as *u8)
92 sys_exit(1); return 1
93}