nx_rebac_gate.nx source

1// nx_rebac_gate.nx -- ADVERSARIAL GATE for the sovereign ReBAC plane (nx_rebac). The CRITIC + ADVERSARY: a 2// legit-access/attack matrix where every escalation, revocation-bypass, cross-scope leak, block-bypass, and 3// userset-cycle MUST resolve correctly (deny-by-default). Green ONLY if all ~28 checks pass. license_tier: ORIGINAL 4// expect_exit: 0 5import "nx_rebac.nx" 6import "nx_gate_verdict.nx" // THE BASE CLASS: gv_ctr/gv_check/gv_verdict make declared == executed 7 8// ONE TOOTH PER CHECK, COUNTED BY THE BASE CLASS (migrated 2026-08-31). THE DEFECT THIS CLOSES: the 9// old ck() set a single okp[0] boolean and the gate ended `verdict=GREEN (28 checks: ...)` with the 28 10// HAND-TYPED IN PROSE. nx_swcompare_evidence.ev_parse_pass looks for `pass=N/M`, `passed N/M` or 11// `PASS=N FAIL=K`; this gate emitted NONE of them, so the evidence layer recorded pass=0/0 and the 12// authz board carried a GREEN on a tooth counter saying ZERO TEETH RAN. A hand-typed 28 is the same 13// fabricated-constant class as a counter emitted but never incremented -- add a check and the prose 14// silently lies. gv_ctr/gv_check make declared == executed BY CONSTRUCTION: the denominator IS the 15// teeth that ran. The ALLOW/DENY diagnostic is KEPT and printed BEFORE the verdict, because a gate 16// that reports a boolean cannot say why. 17func ck(label: *u8, got: i64, want: i64, ctr: *i64) -> i64 { 18 var ok: i64 = 0 19 if got == want { ok = 1 } 20 rb_p(" REBAC got=" as *u8) 21 if got == 1 { rb_p("ALLOW" as *u8) } else { rb_p("DENY " as *u8) } 22 rb_p(" want=" as *u8); rb_pn(want); rb_p(" " as *u8) 23 return gv_check(label, ok, ctr) 24} 25 26func main() -> i64 { 27 rb_p("=== NX-REBAC ADVERSARIAL GATE (Zanzibar/ReBAC: tuple check + userset rewrite + tombstone + block + HR override) ===\n" as *u8) 28 let ctr: *i64 = gv_ctr() // [0]=pass [1]=total [2]=preconditions-missing; the counter IS the denominator 29 30 // fresh store prefix (own the isolation; sys_now_us keeps commits time-ordered for latest-wins) 31 let prefix: *u8 = sys_mmap(128); var po: i64 = 0 32 po = rb_cat(prefix, po, "/tmp/rebac_" as *u8); po = rb_catn(prefix, po, sys_now_us()); po = rb_cat(prefix, po, "_" as *u8); prefix[po] = 0 as u8 33 34 // ---- SETUP (grants) ---- 35 // group:elders owned by alice, bob is a member; doc:budget owned by alice, SHARED with elders#member (userset); 36 // tenant:andelinwest admin=alice member=bob; alice<->bob mutual friends. 37 rb_put(prefix, "group:elders" as *u8, "owner" as *u8, "user:alice" as *u8, "system" as *u8, 1) 38 rb_put(prefix, "group:elders" as *u8, "member" as *u8, "user:bob" as *u8, "user:alice" as *u8, 1) 39 rb_put(prefix, "doc:budget" as *u8, "owner" as *u8, "user:alice" as *u8, "system" as *u8, 1) 40 rb_put(prefix, "doc:budget" as *u8, "viewer" as *u8, "group:elders#member" as *u8, "user:alice" as *u8, 1) 41 rb_put(prefix, "tenant:andelinwest" as *u8, "admin" as *u8, "user:alice" as *u8, "system" as *u8, 1) 42 rb_put(prefix, "tenant:andelinwest" as *u8, "member" as *u8, "user:bob" as *u8, "user:alice" as *u8, 1) 43 rb_put(prefix, "user:alice" as *u8, "friend" as *u8, "user:bob" as *u8, "user:bob" as *u8, 1) 44 rb_put(prefix, "user:bob" as *u8, "friend" as *u8, "user:alice" as *u8, "user:alice" as *u8, 1) 45 46 // ---- ALLOW (legitimate access) ---- 47 ck("A1 alice manage doc:budget (owner)" as *u8, rb_check(prefix, "user:alice" as *u8, "manage" as *u8, "doc:budget" as *u8, 0), 1, ctr) 48 ck("A2 bob read doc:budget (member->elders#member->viewer USERSET)" as *u8, rb_check(prefix, "user:bob" as *u8, "read" as *u8, "doc:budget" as *u8, 0), 1, ctr) 49 ck("A3 alice read doc:budget (owner->read rewrite)" as *u8, rb_check(prefix, "user:alice" as *u8, "read" as *u8, "doc:budget" as *u8, 0), 1, ctr) 50 ck("A4 bob view group:elders (member)" as *u8, rb_check(prefix, "user:bob" as *u8, "view" as *u8, "group:elders" as *u8, 0), 1, ctr) 51 ck("A5 alice manage group:elders (owner)" as *u8, rb_check(prefix, "user:alice" as *u8, "manage" as *u8, "group:elders" as *u8, 0), 1, ctr) 52 ck("A6 bob read tenant:andelinwest (member)" as *u8, rb_check(prefix, "user:bob" as *u8, "read" as *u8, "tenant:andelinwest" as *u8, 0), 1, ctr) 53 ck("A7 alice friend bob (mutual)" as *u8, rb_check(prefix, "user:alice" as *u8, "friend" as *u8, "user:bob" as *u8, 0), 1, ctr) 54 55 // ENUMERATORS (the surface lists a caller's circle from these): alice's friends include bob; bob's groups include elders 56 let el: *i64 = sys_mmap(8 * 64) as *i64 57 let enf: i64 = rb_list_subjects(prefix, "user:alice" as *u8, "friend" as *u8, el, 64) 58 var friend_listed: i64 = 0 59 if enf >= 1 { if rb_in_list(el, enf, "user:bob" as *u8) == 1 { friend_listed = 1 } } 60 ck("E1 rb_list_subjects: alice friends include bob" as *u8, friend_listed, 1, ctr) 61 let eg: *i64 = sys_mmap(8 * 64) as *i64 62 let eng: i64 = rb_list_objects_for_sub(prefix, "user:bob" as *u8, "member" as *u8, eg, 64) 63 var group_listed: i64 = 0 64 if eng >= 1 { if rb_in_list(eg, eng, "group:elders" as *u8) == 1 { group_listed = 1 } } 65 ck("E2 rb_list_objects_for_sub: bob groups include elders" as *u8, group_listed, 1, ctr) 66 67 // ---- DENY (adversary: no grant / wrong relation / escalation) ---- 68 ck("D1 carol read doc:budget (not a member)" as *u8, rb_check(prefix, "user:carol" as *u8, "read" as *u8, "doc:budget" as *u8, 0), 0, ctr) 69 ck("D2 bob WRITE doc:budget (only viewer, not editor)" as *u8, rb_check(prefix, "user:bob" as *u8, "write" as *u8, "doc:budget" as *u8, 0), 0, ctr) 70 ck("D3 mallory read tenant:andelinwest (no grant)" as *u8, rb_check(prefix, "user:mallory" as *u8, "read" as *u8, "tenant:andelinwest" as *u8, 0), 0, ctr) 71 ck("D4 bob MANAGE group:elders (member != admin ESCALATION)" as *u8, rb_check(prefix, "user:bob" as *u8, "manage" as *u8, "group:elders" as *u8, 0), 0, ctr) 72 ck("D5 carol friend alice (not friends)" as *u8, rb_check(prefix, "user:carol" as *u8, "friend" as *u8, "user:alice" as *u8, 0), 0, ctr) 73 74 // ---- REVOCATION (tombstone must WIN; scoped, not global) ---- 75 // T1 defriend: tombstone both directions -> no longer friends 76 rb_put(prefix, "user:alice" as *u8, "friend" as *u8, "user:bob" as *u8, "user:alice" as *u8, 0) 77 rb_put(prefix, "user:bob" as *u8, "friend" as *u8, "user:alice" as *u8, "user:bob" as *u8, 0) 78 ck("T1 defriended: alice friend bob (tombstone wins)" as *u8, rb_check(prefix, "user:alice" as *u8, "friend" as *u8, "user:bob" as *u8, 0), 0, ctr) 79 // T2 leave group: bob leaves elders -> loses doc VIA the group, but KEEPS the independent tenant membership 80 rb_put(prefix, "group:elders" as *u8, "member" as *u8, "user:bob" as *u8, "user:bob" as *u8, 0) 81 ck("T2a left-group: bob read doc:budget (userset re-eval DENIES)" as *u8, rb_check(prefix, "user:bob" as *u8, "read" as *u8, "doc:budget" as *u8, 0), 0, ctr) 82 ck("T2b scoped: bob read tenant:andelinwest STILL allowed" as *u8, rb_check(prefix, "user:bob" as *u8, "read" as *u8, "tenant:andelinwest" as *u8, 0), 1, ctr) 83 // T3 re-grant then unshare: re-join proves re-grant works; unshare the doc-userset kills it again 84 rb_put(prefix, "group:elders" as *u8, "member" as *u8, "user:bob" as *u8, "user:alice" as *u8, 1) 85 ck("T3a re-joined: bob read doc:budget allowed again (re-grant)" as *u8, rb_check(prefix, "user:bob" as *u8, "read" as *u8, "doc:budget" as *u8, 0), 1, ctr) 86 rb_put(prefix, "doc:budget" as *u8, "viewer" as *u8, "group:elders#member" as *u8, "user:alice" as *u8, 0) 87 ck("T3b unshared: bob read doc:budget DENIED (userset tombstone)" as *u8, rb_check(prefix, "user:bob" as *u8, "read" as *u8, "doc:budget" as *u8, 0), 0, ctr) 88 89 // ---- BLOCK (consent axis: blocks OUTRANK any relation) ---- 90 rb_put(prefix, "user:bob" as *u8, "blocked" as *u8, "user:mallory" as *u8, "user:bob" as *u8, 1) 91 ck("B1 mallory friend bob after BLOCK (blocks outrank)" as *u8, rb_check(prefix, "user:mallory" as *u8, "friend" as *u8, "user:bob" as *u8, 0), 0, ctr) 92 ck("B2 mallory view bob after BLOCK" as *u8, rb_check(prefix, "user:mallory" as *u8, "view" as *u8, "user:bob" as *u8, 0), 0, ctr) 93 94 // ---- HR OPERATOR OVERRIDE (the tie to Nishi HR level) ---- 95 ck("H1 mallory read tenant via HR operator lvl 3 (god-in-realm)" as *u8, rb_check_hr(prefix, "user:mallory" as *u8, "read" as *u8, "tenant:andelinwest" as *u8, 3), 1, ctr) 96 ck("H2 mallory read tenant via HR member lvl 1 (no tuple -> deny)" as *u8, rb_check_hr(prefix, "user:mallory" as *u8, "read" as *u8, "tenant:andelinwest" as *u8, 1), 0, ctr) 97 98 // ---- WRITE AUTHORITY (a member cannot grant; unclaimed object bootstraps; then closes) ---- 99 ck("W1 bob may_grant doc:budget (viewer, not manage -> NO)" as *u8, rb_may_grant(prefix, "user:bob" as *u8, "doc:budget" as *u8), 0, ctr) 100 ck("W2 alice may_grant doc:budget (owner -> YES)" as *u8, rb_may_grant(prefix, "user:alice" as *u8, "doc:budget" as *u8), 1, ctr) 101 ck("W3a carol may_grant group:new (UNCLAIMED -> bootstrap YES)" as *u8, rb_may_grant(prefix, "user:carol" as *u8, "group:new" as *u8), 1, ctr) 102 rb_put(prefix, "group:new" as *u8, "owner" as *u8, "user:carol" as *u8, "user:carol" as *u8, 1) 103 ck("W3b mallory may_grant group:new (now CLAIMED by carol -> NO)" as *u8, rb_may_grant(prefix, "user:mallory" as *u8, "group:new" as *u8), 0, ctr) 104 105 // ---- NESTED USERSET (positive, multi-level): leads subgroup nested in elders, doc shared with elders ---- 106 rb_put(prefix, "group:leads" as *u8, "member" as *u8, "user:carol" as *u8, "user:carol" as *u8, 1) 107 rb_put(prefix, "group:elders" as *u8, "member" as *u8, "group:leads#member" as *u8, "user:alice" as *u8, 1) 108 rb_put(prefix, "doc:plan" as *u8, "owner" as *u8, "user:alice" as *u8, "system" as *u8, 1) 109 rb_put(prefix, "doc:plan" as *u8, "viewer" as *u8, "group:elders#member" as *u8, "user:alice" as *u8, 1) 110 ck("U1 carol read doc:plan (carol->leads->elders->doc NESTED userset)" as *u8, rb_check(prefix, "user:carol" as *u8, "read" as *u8, "doc:plan" as *u8, 0), 1, ctr) 111 112 // ---- CYCLE TERMINATION (adversary DoS: mutual group membership must NOT hang) ---- 113 rb_put(prefix, "group:ca" as *u8, "member" as *u8, "group:cb#member" as *u8, "user:alice" as *u8, 1) 114 rb_put(prefix, "group:cb" as *u8, "member" as *u8, "group:ca#member" as *u8, "user:alice" as *u8, 1) 115 ck("C1 cyclic groups TERMINATE (mallory read group:ca -> bounded DENY, no hang)" as *u8, rb_check(prefix, "user:mallory" as *u8, "read" as *u8, "group:ca" as *u8, 0), 0, ctr) 116 117 // ---- CROSS-SURFACE (rb_check2, two stores): a GROUP in store2 grants an OBJECT owned in store1 ---- 118 let p2: *u8 = sys_mmap(128); var p2o: i64 = 0 119 p2o = rb_cat(p2, p2o, "/tmp/rebac2_" as *u8); p2o = rb_catn(p2, p2o, sys_now_us()); p2o = rb_cat(p2, p2o, "_" as *u8); p2[p2o] = 0 as u8 120 rb_put(p2, "group:choir" as *u8, "member" as *u8, "user:zoe" as *u8, "user:lead" as *u8, 1) // store2 = the "relate" surface 121 rb_put(prefix, "doc:hymnal" as *u8, "owner" as *u8, "user:lead" as *u8, "system" as *u8, 1) // store1 = the "office" surface 122 rb_put(prefix, "doc:hymnal" as *u8, "viewer" as *u8, "group:choir#member" as *u8, "user:lead" as *u8, 1) 123 ck("X1 CROSS-SURFACE: zoe (store2 group member) reads doc in store1" as *u8, rb_check2(prefix, p2, "user:zoe" as *u8, "read" as *u8, "doc:hymnal" as *u8, 0), 1, ctr) 124 ck("X2 non-member frank DENIED cross-surface" as *u8, rb_check2(prefix, p2, "user:frank" as *u8, "read" as *u8, "doc:hymnal" as *u8, 0), 0, ctr) 125 rb_put(p2, "group:choir" as *u8, "member" as *u8, "user:zoe" as *u8, "user:lead" as *u8, 0) // revoke in store2 126 ck("X3 revoke store2 group membership -> zoe LOSES the store1 doc" as *u8, rb_check2(prefix, p2, "user:zoe" as *u8, "read" as *u8, "doc:hymnal" as *u8, 0), 0, ctr) 127 128 // THE VERDICT NOTE NO LONGER RECITES THE TEETH. gv_verdict prints `passed <p>/<t>` from the 129 // counter that actually ran them, so a check added tomorrow cannot make this line lie -- the old 130 // note's hand-typed "28 checks" was a fabricated constant wearing the shape of a measurement, and 131 // it was the ONLY place this gate ever stated a denominator. 132 return gv_verdict("REBAC-GATE" as *u8, ctr, "userset rewrites + nested groups + tombstone revocation + scoped-not-global + blocks-outrank + HR operator override + write-authority-no-escalation + cycle-termination" as *u8) 133}