556 lines
21 KiB
JavaScript
556 lines
21 KiB
JavaScript
|
|
/**
|
||
|
|
* rigor/zanzibar-semantics.test.js — js-rigor property tests for
|
||
|
|
* Zanzibar-style authorization graph semantics.
|
||
|
|
*
|
||
|
|
* Zanzibar's core model (Google's global authorization system):
|
||
|
|
* relation tuples (object, relation, user), usersets, and rewrite rules
|
||
|
|
* (direct, tuple-to-userset, union, intersection, exclusion).
|
||
|
|
*
|
||
|
|
* Properties verified:
|
||
|
|
*
|
||
|
|
* - UNION: a grant from ANY child grants at the child's possibility
|
||
|
|
* (max over children); no child grants → deny.
|
||
|
|
* - INTERSECTION: ALL children must grant; result is the min.
|
||
|
|
* - EXCLUSION (A AND NOT B): the denied set blocks the allowed set;
|
||
|
|
* p = pA * (1 - pB).
|
||
|
|
* - EXPAND PARITY (flagship): a brute-force reference implementation of
|
||
|
|
* Zanzibar's Expand RPC (userset expansion) is compared against
|
||
|
|
* arbiter.check() over RANDOM graphs with random rewrite configs —
|
||
|
|
* direct, chain (transitive member_of), tuple-to-userset, union and
|
||
|
|
* exclusion — with random edge possibilities including 0.
|
||
|
|
* - NESTED CHAIN: membership transitivity through N nested groups honors
|
||
|
|
* the weakest link (min possibility along the full path).
|
||
|
|
* - CYCLE SAFETY: cyclic membership graphs terminate and never create
|
||
|
|
* spurious access.
|
||
|
|
*/
|
||
|
|
import { describe, it } from 'node:test';
|
||
|
|
import assert from 'node:assert/strict';
|
||
|
|
import { rigor } from '@rigor/core';
|
||
|
|
import { Arbiter } from '../../src/index.js';
|
||
|
|
|
||
|
|
const EPS = 1e-9;
|
||
|
|
const POSSIBILITIES = [0, 0.25, 0.5, 0.75, 1];
|
||
|
|
|
||
|
|
function fail(message) {
|
||
|
|
throw new Error(message);
|
||
|
|
}
|
||
|
|
|
||
|
|
/**
|
||
|
|
* Reference implementation of Zanzibar's Expand RPC over a graph of
|
||
|
|
* users / groups / one object, for the rewrite configs the engine supports.
|
||
|
|
* Returns the possibility that `user` is in the userset of (object, rel).
|
||
|
|
*
|
||
|
|
* Semantics mirrored from the engine (verified empirically):
|
||
|
|
* - direct: only edges whose subject is the user itself (no implicit
|
||
|
|
* group expansion on direct tuples); possibility = edge possibility.
|
||
|
|
* - chain: transitive `member_of` traversal (min along path, max over
|
||
|
|
* paths), then a final edge of the terminal relation into the object.
|
||
|
|
* - tuple_to_userset: object's tuplesetRelation edges (doc → group),
|
||
|
|
* joined with a DIRECT computedRelation edge from the user; min.
|
||
|
|
* - union: max over children. intersection: min over children.
|
||
|
|
* - exclusion: pA * (1 - pB).
|
||
|
|
*/
|
||
|
|
export function buildExpandOracle(graph, config) {
|
||
|
|
const { memberOf, edgesByRelation } = graph;
|
||
|
|
const edges = (rel) => edgesByRelation.get(rel) || [];
|
||
|
|
|
||
|
|
function directUserset(rel) {
|
||
|
|
return (userId) => {
|
||
|
|
let best = 0;
|
||
|
|
// direct edges point FROM the subject TO the object (src=subject, dst=object)
|
||
|
|
for (const e of edges(rel)) {
|
||
|
|
if (e.from === userId && e.subject === graph.objectId) {
|
||
|
|
if (e.p > best) best = e.p;
|
||
|
|
}
|
||
|
|
}
|
||
|
|
return best;
|
||
|
|
};
|
||
|
|
}
|
||
|
|
|
||
|
|
function transitiveMembers(userId) {
|
||
|
|
// BFS over member_of edges; min possibility along each path; max over paths.
|
||
|
|
const best = new Map([[userId, 1]]);
|
||
|
|
const queue = [userId];
|
||
|
|
while (queue.length) {
|
||
|
|
const node = queue.shift();
|
||
|
|
const nodeP = best.get(node);
|
||
|
|
for (const e of edges('member_of')) {
|
||
|
|
if (e.from !== node) continue;
|
||
|
|
const nextP = Math.min(nodeP, e.p);
|
||
|
|
const prev = best.get(e.subject);
|
||
|
|
if (prev === undefined || nextP > prev) {
|
||
|
|
best.set(e.subject, nextP);
|
||
|
|
queue.push(e.subject);
|
||
|
|
}
|
||
|
|
}
|
||
|
|
}
|
||
|
|
return best;
|
||
|
|
}
|
||
|
|
|
||
|
|
function reachAtExactHops(userId, hops) {
|
||
|
|
// Nodes reachable in EXACTLY `hops` member_of traversals, with the
|
||
|
|
// best (max) possibility per node. Mirrors the engine's per-step
|
||
|
|
// path extension (paths always traverse every step).
|
||
|
|
let frontier = new Map([[userId, 1]]);
|
||
|
|
for (let h = 0; h < hops; h++) {
|
||
|
|
const next = new Map();
|
||
|
|
for (const [node, nodeP] of frontier) {
|
||
|
|
for (const e of edges('member_of')) {
|
||
|
|
if (e.from !== node) continue;
|
||
|
|
const nextP = Math.min(nodeP, e.p);
|
||
|
|
const prev = next.get(e.subject);
|
||
|
|
if (prev === undefined || nextP > prev) {
|
||
|
|
next.set(e.subject, nextP);
|
||
|
|
}
|
||
|
|
}
|
||
|
|
}
|
||
|
|
frontier = next;
|
||
|
|
if (frontier.size === 0) break;
|
||
|
|
}
|
||
|
|
return frontier;
|
||
|
|
}
|
||
|
|
|
||
|
|
function evalRule(rule, userId) {
|
||
|
|
if (rule.type === 'direct') {
|
||
|
|
return directUserset(rule.relation)(userId);
|
||
|
|
}
|
||
|
|
if (rule.type === 'chain') {
|
||
|
|
// steps: N member_of hops then a terminal relation into the object.
|
||
|
|
// The engine extends paths through EVERY step, so the terminal edge
|
||
|
|
// may only originate from nodes reachable in exactly N member_of hops
|
||
|
|
// (the starting user alone never satisfies the chain).
|
||
|
|
const steps = rule.steps;
|
||
|
|
const terminal = steps[steps.length - 1].relation;
|
||
|
|
const memberHops = steps.length - 1;
|
||
|
|
let best = 0;
|
||
|
|
if (memberHops > 0) {
|
||
|
|
for (const [node, p] of reachAtExactHops(userId, memberHops)) {
|
||
|
|
for (const e of edges(terminal)) {
|
||
|
|
if (e.from === node && e.subject === graph.objectId) {
|
||
|
|
const pathP = Math.min(p, e.p);
|
||
|
|
if (pathP > best) best = pathP;
|
||
|
|
}
|
||
|
|
}
|
||
|
|
}
|
||
|
|
}
|
||
|
|
return best;
|
||
|
|
}
|
||
|
|
if (rule.type === 'tuple_to_userset') {
|
||
|
|
let best = 0;
|
||
|
|
for (const t of edges(rule.tuplesetRelation)) {
|
||
|
|
if (t.from !== graph.objectId) continue;
|
||
|
|
// computed side is a DIRECT relation lookup (verified semantics)
|
||
|
|
let memberP = 0;
|
||
|
|
for (const m of edges(rule.computedRelation)) {
|
||
|
|
if (m.from === userId && m.subject === t.subject) {
|
||
|
|
if (m.p > memberP) memberP = m.p;
|
||
|
|
}
|
||
|
|
}
|
||
|
|
const combined = Math.min(t.p, memberP);
|
||
|
|
if (combined > best) best = combined;
|
||
|
|
}
|
||
|
|
return best;
|
||
|
|
}
|
||
|
|
if (rule.union) {
|
||
|
|
return Math.max(0, ...rule.union.map((r) => evalRule(r, userId)));
|
||
|
|
}
|
||
|
|
if (rule.intersection) {
|
||
|
|
return Math.min(...rule.intersection.map((r) => evalRule(r, userId)));
|
||
|
|
}
|
||
|
|
if (rule.exclusion) {
|
||
|
|
const [a, b] = rule.exclusion;
|
||
|
|
return evalRule(a, userId) * (1 - evalRule(b, userId));
|
||
|
|
}
|
||
|
|
return 0;
|
||
|
|
}
|
||
|
|
|
||
|
|
return { evalRule };
|
||
|
|
}
|
||
|
|
|
||
|
|
/**
|
||
|
|
* Build a random Zanzibar-style graph + rewrite config, and the matching
|
||
|
|
* Arbiter instance. Config shapes are chosen from a fixed family so the
|
||
|
|
* oracle and the engine stay in sync by construction.
|
||
|
|
*/
|
||
|
|
export function buildRandomZanzibarCase(seedCase) {
|
||
|
|
const { userCount, groupCount, configKind } = seedCase;
|
||
|
|
const users = Array.from({ length: userCount }, (_, i) => `user:${i}`);
|
||
|
|
const groups = Array.from({ length: groupCount }, (_, i) => `group:${i}`);
|
||
|
|
const allSubjects = [...users, ...groups];
|
||
|
|
const doc = 'doc:1';
|
||
|
|
|
||
|
|
const arbiter = new Arbiter();
|
||
|
|
for (const u of users) arbiter.addNode(u, 'user');
|
||
|
|
for (const g of groups) arbiter.addNode(g, 'group');
|
||
|
|
arbiter.addNode(doc, 'doc');
|
||
|
|
arbiter.setRelationConfig('member_of', { type: 'direct' });
|
||
|
|
|
||
|
|
const edgesByRelation = new Map();
|
||
|
|
const addEdge = (rel, from, subject, p) => {
|
||
|
|
let list = edgesByRelation.get(rel);
|
||
|
|
if (!list) {
|
||
|
|
list = [];
|
||
|
|
edgesByRelation.set(rel, list);
|
||
|
|
}
|
||
|
|
// The engine dedups relations per (src, rel, dst) with last-write-wins
|
||
|
|
// (addRelation updates an existing tuple). Mirror that so the oracle
|
||
|
|
// and the engine observe identical edge data.
|
||
|
|
const existing = list.find((e) => e.from === from && e.subject === subject);
|
||
|
|
if (existing) {
|
||
|
|
existing.p = p;
|
||
|
|
arbiter.removeRelation(from, rel, subject);
|
||
|
|
}
|
||
|
|
list.push(existing || { from, subject, p });
|
||
|
|
arbiter.addRelation(from, rel, subject, { possibility: p });
|
||
|
|
};
|
||
|
|
|
||
|
|
const pick = (arr) => arr[Math.floor(Math.random() * arr.length)];
|
||
|
|
|
||
|
|
// member_of edges: users AND groups can be members (nesting), subjects can be groups
|
||
|
|
const memberEdges = Math.max(1, Math.floor((userCount + groupCount) / 2));
|
||
|
|
for (let i = 0; i < memberEdges; i++) {
|
||
|
|
const from = pick(allSubjects);
|
||
|
|
const subject = pick(groups);
|
||
|
|
addEdge('member_of', from, subject, pick(POSSIBILITIES));
|
||
|
|
}
|
||
|
|
|
||
|
|
// Two direct relations (for union / exclusion / direct configs)
|
||
|
|
const d1 = 'viewer_allowed';
|
||
|
|
const d2 = 'viewer_staff';
|
||
|
|
const denied = 'viewer_denied';
|
||
|
|
for (const rel of [d1, d2, denied]) {
|
||
|
|
arbiter.setRelationConfig(rel, { type: 'direct' });
|
||
|
|
}
|
||
|
|
const directEdgeCount = Math.max(1, Math.floor(userCount / 2) + 1);
|
||
|
|
for (let i = 0; i < directEdgeCount; i++) {
|
||
|
|
// direct edges point FROM the subject TO the object (src=subject, dst=doc)
|
||
|
|
addEdge(pick([d1, d2]), pick(allSubjects), doc, pick(POSSIBILITIES));
|
||
|
|
addEdge(denied, pick(allSubjects), doc, pick(POSSIBILITIES));
|
||
|
|
}
|
||
|
|
|
||
|
|
// Tupleset relation: doc → group (for tuple_to_userset)
|
||
|
|
const t1 = 'owner';
|
||
|
|
arbiter.setRelationConfig(t1, { type: 'direct' });
|
||
|
|
if (groupCount > 0) {
|
||
|
|
for (let i = 0; i < groupCount; i++) {
|
||
|
|
addEdge(t1, doc, pick(groups), pick(POSSIBILITIES));
|
||
|
|
}
|
||
|
|
}
|
||
|
|
|
||
|
|
const directRule = () => ({ type: 'direct', relation: pick([d1, d2]) });
|
||
|
|
const chainRule = () => ({
|
||
|
|
type: 'chain',
|
||
|
|
steps: [
|
||
|
|
{ relation: 'member_of', direction: 'out' },
|
||
|
|
{ relation: 'member_of', direction: 'out' },
|
||
|
|
{ relation: pick([d1, d2]), direction: 'out' }
|
||
|
|
]
|
||
|
|
});
|
||
|
|
const ttuRule = () => ({
|
||
|
|
type: 'tuple_to_userset',
|
||
|
|
tuplesetRelation: t1,
|
||
|
|
computedRelation: 'member_of',
|
||
|
|
reverse: false
|
||
|
|
});
|
||
|
|
const allowRule = () => pick([directRule(), chainRule(), ttuRule()]);
|
||
|
|
|
||
|
|
let config;
|
||
|
|
if (configKind === 0) config = allowRule();
|
||
|
|
else if (configKind === 1) config = { union: [allowRule(), allowRule()] };
|
||
|
|
else if (configKind === 2) config = { intersection: [allowRule(), allowRule()] };
|
||
|
|
else if (configKind === 3) config = { exclusion: [allowRule(), { type: 'direct', relation: denied }] };
|
||
|
|
else config = { union: [allowRule(), { exclusion: [allowRule(), { type: 'direct', relation: denied }] }] };
|
||
|
|
|
||
|
|
arbiter.setRelationConfig('viewer', config);
|
||
|
|
return {
|
||
|
|
arbiter,
|
||
|
|
graph: {
|
||
|
|
objectId: doc,
|
||
|
|
memberOf: edgesByRelation.get('member_of') || [],
|
||
|
|
edgesByRelation
|
||
|
|
},
|
||
|
|
config,
|
||
|
|
users
|
||
|
|
};
|
||
|
|
}
|
||
|
|
|
||
|
|
describe('Zanzibar rewrite-rule semantics (rigor)', () => {
|
||
|
|
it('UNION: max over children — any grant grants, none denies', async () => {
|
||
|
|
async function check({ pa, pb, hasA, hasB }) {
|
||
|
|
const arbiter = new Arbiter();
|
||
|
|
['user:u', 'doc:1'].forEach((k) => arbiter.addNode(k, k.startsWith('user') ? 'user' : 'doc'));
|
||
|
|
arbiter.setRelationConfig('rel_a', { type: 'direct' });
|
||
|
|
arbiter.setRelationConfig('rel_b', { type: 'direct' });
|
||
|
|
arbiter.setRelationConfig('viewer', {
|
||
|
|
union: [
|
||
|
|
{ type: 'direct', relation: 'rel_a' },
|
||
|
|
{ type: 'direct', relation: 'rel_b' }
|
||
|
|
]
|
||
|
|
});
|
||
|
|
if (hasA) arbiter.addRelation('user:u', 'rel_a', 'doc:1', { possibility: pa });
|
||
|
|
if (hasB) arbiter.addRelation('user:u', 'rel_b', 'doc:1', { possibility: pb });
|
||
|
|
|
||
|
|
const result = arbiter.check('user:u', 'viewer', 'doc:1');
|
||
|
|
const expected = Math.max(hasA ? pa : 0, hasB ? pb : 0);
|
||
|
|
if (Math.abs(result.possibility - expected) > EPS) {
|
||
|
|
fail(`union: expected ${expected}, got ${result.possibility}`);
|
||
|
|
}
|
||
|
|
return result;
|
||
|
|
}
|
||
|
|
|
||
|
|
const report = await rigor.campaign(
|
||
|
|
[
|
||
|
|
rigor.fn('check', check, rigor.args(
|
||
|
|
rigor.gen.object({
|
||
|
|
pa: rigor.gen.oneOf(POSSIBILITIES),
|
||
|
|
pb: rigor.gen.oneOf(POSSIBILITIES),
|
||
|
|
hasA: rigor.gen.boolean(),
|
||
|
|
hasB: rigor.gen.boolean()
|
||
|
|
})
|
||
|
|
))
|
||
|
|
],
|
||
|
|
rigor.crucible([
|
||
|
|
rigor.invariant('union-max', ({ error, errorMessage }) => !error && !errorMessage)
|
||
|
|
])
|
||
|
|
).run({ effort: 400, seed: 'zanzibar-union' });
|
||
|
|
|
||
|
|
const inv = report.crucibleVerdict?.invariants?.find(i => i.name === 'union-max');
|
||
|
|
assert.ok(inv);
|
||
|
|
assert.equal(inv.passed, true, `UNION contract violated in ${inv.failureCount} cases`);
|
||
|
|
});
|
||
|
|
|
||
|
|
it('INTERSECTION: min over children — all must grant', async () => {
|
||
|
|
async function check({ pa, pb, hasA, hasB }) {
|
||
|
|
const arbiter = new Arbiter();
|
||
|
|
['user:u', 'doc:1'].forEach((k) => arbiter.addNode(k, k.startsWith('user') ? 'user' : 'doc'));
|
||
|
|
arbiter.setRelationConfig('rel_a', { type: 'direct' });
|
||
|
|
arbiter.setRelationConfig('rel_b', { type: 'direct' });
|
||
|
|
arbiter.setRelationConfig('viewer', {
|
||
|
|
intersection: [
|
||
|
|
{ type: 'direct', relation: 'rel_a' },
|
||
|
|
{ type: 'direct', relation: 'rel_b' }
|
||
|
|
]
|
||
|
|
});
|
||
|
|
if (hasA) arbiter.addRelation('user:u', 'rel_a', 'doc:1', { possibility: pa });
|
||
|
|
if (hasB) arbiter.addRelation('user:u', 'rel_b', 'doc:1', { possibility: pb });
|
||
|
|
|
||
|
|
const result = arbiter.check('user:u', 'viewer', 'doc:1');
|
||
|
|
const expected = Math.min(hasA ? pa : 0, hasB ? pb : 0);
|
||
|
|
if (Math.abs(result.possibility - expected) > EPS) {
|
||
|
|
fail(`intersection: expected ${expected}, got ${result.possibility}`);
|
||
|
|
}
|
||
|
|
return result;
|
||
|
|
}
|
||
|
|
|
||
|
|
const report = await rigor.campaign(
|
||
|
|
[
|
||
|
|
rigor.fn('check', check, rigor.args(
|
||
|
|
rigor.gen.object({
|
||
|
|
pa: rigor.gen.oneOf(POSSIBILITIES),
|
||
|
|
pb: rigor.gen.oneOf(POSSIBILITIES),
|
||
|
|
hasA: rigor.gen.boolean(),
|
||
|
|
hasB: rigor.gen.boolean()
|
||
|
|
})
|
||
|
|
))
|
||
|
|
],
|
||
|
|
rigor.crucible([
|
||
|
|
rigor.invariant('intersection-min', ({ error, errorMessage }) => !error && !errorMessage)
|
||
|
|
])
|
||
|
|
).run({ effort: 400, seed: 'zanzibar-intersection' });
|
||
|
|
|
||
|
|
const inv = report.crucibleVerdict?.invariants?.find(i => i.name === 'intersection-min');
|
||
|
|
assert.ok(inv);
|
||
|
|
assert.equal(inv.passed, true, `INTERSECTION contract violated in ${inv.failureCount} cases`);
|
||
|
|
});
|
||
|
|
|
||
|
|
it('EXCLUSION (A AND NOT B): denied set blocks the allowed set', async () => {
|
||
|
|
async function check({ pa, pb, denied }) {
|
||
|
|
const arbiter = new Arbiter();
|
||
|
|
['user:u', 'doc:1'].forEach((k) => arbiter.addNode(k, k.startsWith('user') ? 'user' : 'doc'));
|
||
|
|
arbiter.setRelationConfig('rel_a', { type: 'direct' });
|
||
|
|
arbiter.setRelationConfig('rel_b', { type: 'direct' });
|
||
|
|
arbiter.setRelationConfig('viewer', {
|
||
|
|
exclusion: [
|
||
|
|
{ type: 'direct', relation: 'rel_a' },
|
||
|
|
{ type: 'direct', relation: 'rel_b' }
|
||
|
|
]
|
||
|
|
});
|
||
|
|
arbiter.addRelation('user:u', 'rel_a', 'doc:1', { possibility: pa });
|
||
|
|
if (denied) arbiter.addRelation('user:u', 'rel_b', 'doc:1', { possibility: pb });
|
||
|
|
|
||
|
|
const result = arbiter.check('user:u', 'viewer', 'doc:1');
|
||
|
|
const expected = pa * (1 - (denied ? pb : 0));
|
||
|
|
if (Math.abs(result.possibility - expected) > EPS) {
|
||
|
|
fail(`exclusion: expected ${expected}, got ${result.possibility}`);
|
||
|
|
}
|
||
|
|
return result;
|
||
|
|
}
|
||
|
|
|
||
|
|
const report = await rigor.campaign(
|
||
|
|
[
|
||
|
|
rigor.fn('check', check, rigor.args(
|
||
|
|
rigor.gen.object({
|
||
|
|
pa: rigor.gen.oneOf(POSSIBILITIES),
|
||
|
|
pb: rigor.gen.oneOf(POSSIBILITIES),
|
||
|
|
denied: rigor.gen.boolean()
|
||
|
|
})
|
||
|
|
))
|
||
|
|
],
|
||
|
|
rigor.crucible([
|
||
|
|
rigor.invariant('exclusion-blocks', ({ error, errorMessage }) => !error && !errorMessage)
|
||
|
|
])
|
||
|
|
).run({ effort: 400, seed: 'zanzibar-exclusion' });
|
||
|
|
|
||
|
|
const inv = report.crucibleVerdict?.invariants?.find(i => i.name === 'exclusion-blocks');
|
||
|
|
assert.ok(inv);
|
||
|
|
assert.equal(inv.passed, true, `EXCLUSION contract violated in ${inv.failureCount} cases`);
|
||
|
|
});
|
||
|
|
|
||
|
|
it('EXPAND PARITY: check() agrees with the Expand-RPC oracle on random graphs', async () => {
|
||
|
|
async function check(caseParams) {
|
||
|
|
const { arbiter, graph, config, users } = buildRandomZanzibarCase(caseParams);
|
||
|
|
const oracle = buildExpandOracle(graph, config);
|
||
|
|
|
||
|
|
for (const user of users) {
|
||
|
|
const expected = oracle.evalRule(config, user);
|
||
|
|
const actual = arbiter.check(user, 'viewer', graph.objectId);
|
||
|
|
if (Math.abs(actual.possibility - expected) > EPS) {
|
||
|
|
fail(`expand parity for ${user}: oracle=${expected}, engine=${actual.possibility}`);
|
||
|
|
}
|
||
|
|
}
|
||
|
|
return { checked: users.length };
|
||
|
|
}
|
||
|
|
|
||
|
|
const report = await rigor.campaign(
|
||
|
|
[
|
||
|
|
rigor.fn('check', check, rigor.args(
|
||
|
|
rigor.gen.object({
|
||
|
|
userCount: rigor.gen.int(1, 4),
|
||
|
|
groupCount: rigor.gen.int(0, 4),
|
||
|
|
configKind: rigor.gen.int(0, 4)
|
||
|
|
})
|
||
|
|
))
|
||
|
|
],
|
||
|
|
rigor.crucible([
|
||
|
|
rigor.invariant('expand-parity', ({ error, errorMessage }) => !error && !errorMessage)
|
||
|
|
])
|
||
|
|
).run({ effort: 800, seed: 'zanzibar-expand-parity' });
|
||
|
|
|
||
|
|
const inv = report.crucibleVerdict?.invariants?.find(i => i.name === 'expand-parity');
|
||
|
|
assert.ok(inv);
|
||
|
|
assert.equal(inv.passed, true, `EXPAND PARITY violated in ${inv.failureCount} cases`);
|
||
|
|
});
|
||
|
|
|
||
|
|
it('NESTED CHAIN: transitivity through N groups honors the weakest link', async () => {
|
||
|
|
async function check({ depth, ps }) {
|
||
|
|
const arbiter = new Arbiter();
|
||
|
|
arbiter.addNode('user:alice', 'user');
|
||
|
|
arbiter.addNode('doc:1', 'doc');
|
||
|
|
const groupKeys = [];
|
||
|
|
for (let i = 0; i < depth; i++) {
|
||
|
|
const key = `group:${i}`;
|
||
|
|
groupKeys.push(key);
|
||
|
|
arbiter.addNode(key, 'group');
|
||
|
|
}
|
||
|
|
arbiter.setRelationConfig('member_of', { type: 'direct' });
|
||
|
|
arbiter.setRelationConfig('viewer', { type: 'direct' });
|
||
|
|
const steps = [];
|
||
|
|
for (let i = 0; i < depth; i++) {
|
||
|
|
steps.push({ relation: 'member_of', direction: 'out' });
|
||
|
|
}
|
||
|
|
steps.push({ relation: 'viewer', direction: 'out' });
|
||
|
|
arbiter.setRelationConfig('can_access', { type: 'chain', steps });
|
||
|
|
|
||
|
|
let from = 'user:alice';
|
||
|
|
let expected = 1;
|
||
|
|
for (let i = 0; i < depth; i++) {
|
||
|
|
arbiter.addRelation(from, 'member_of', groupKeys[i], { possibility: ps[i] });
|
||
|
|
expected = Math.min(expected, ps[i]);
|
||
|
|
from = groupKeys[i];
|
||
|
|
}
|
||
|
|
arbiter.addRelation(from, 'viewer', 'doc:1', { possibility: ps[depth] });
|
||
|
|
expected = Math.min(expected, ps[depth]);
|
||
|
|
|
||
|
|
const result = arbiter.check('user:alice', 'can_access', 'doc:1');
|
||
|
|
if (Math.abs(result.possibility - expected) > EPS) {
|
||
|
|
fail(`nested chain depth ${depth}: expected ${expected}, got ${result.possibility}`);
|
||
|
|
}
|
||
|
|
return result;
|
||
|
|
}
|
||
|
|
|
||
|
|
const report = await rigor.campaign(
|
||
|
|
[
|
||
|
|
rigor.fn('check', check, rigor.args(
|
||
|
|
rigor.gen.object({
|
||
|
|
depth: rigor.gen.int(1, 5),
|
||
|
|
ps: rigor.gen.array(rigor.gen.oneOf(POSSIBILITIES), 2, 6)
|
||
|
|
})
|
||
|
|
))
|
||
|
|
],
|
||
|
|
rigor.crucible([
|
||
|
|
rigor.invariant('nested-weakest-link', ({ error, errorMessage }) => !error && !errorMessage)
|
||
|
|
])
|
||
|
|
).run({ effort: 500, seed: 'zanzibar-nested-chain' });
|
||
|
|
|
||
|
|
const inv = report.crucibleVerdict?.invariants?.find(i => i.name === 'nested-weakest-link');
|
||
|
|
assert.ok(inv);
|
||
|
|
assert.equal(inv.passed, true, `NESTED CHAIN contract violated in ${inv.failureCount} cases`);
|
||
|
|
});
|
||
|
|
|
||
|
|
it('CYCLE SAFETY: cyclic memberships terminate and never fabricate access', async () => {
|
||
|
|
async function check({ cycleSize, memberP }) {
|
||
|
|
const arbiter = new Arbiter();
|
||
|
|
arbiter.addNode('user:alice', 'user');
|
||
|
|
arbiter.addNode('doc:1', 'doc');
|
||
|
|
const groups = [];
|
||
|
|
for (let i = 0; i < cycleSize; i++) {
|
||
|
|
const key = `group:${i}`;
|
||
|
|
groups.push(key);
|
||
|
|
arbiter.addNode(key, 'group');
|
||
|
|
}
|
||
|
|
arbiter.setRelationConfig('member_of', { type: 'direct' });
|
||
|
|
arbiter.setRelationConfig('viewer', { type: 'direct' });
|
||
|
|
arbiter.setRelationConfig('can_access', {
|
||
|
|
type: 'chain',
|
||
|
|
steps: [
|
||
|
|
{ relation: 'member_of', direction: 'out' },
|
||
|
|
{ relation: 'member_of', direction: 'out' },
|
||
|
|
{ relation: 'viewer', direction: 'out' }
|
||
|
|
]
|
||
|
|
});
|
||
|
|
|
||
|
|
// Closed cycle: g0 → g1 → ... → g0 (no user attached, no doc access)
|
||
|
|
for (let i = 0; i < cycleSize; i++) {
|
||
|
|
const next = groups[(i + 1) % cycleSize];
|
||
|
|
arbiter.addRelation(groups[i], 'member_of', next, { possibility: memberP });
|
||
|
|
}
|
||
|
|
// A user attached to the cycle must not gain access to the doc
|
||
|
|
arbiter.addRelation('user:alice', 'member_of', groups[0], { possibility: memberP });
|
||
|
|
|
||
|
|
const result = arbiter.check('user:alice', 'can_access', 'doc:1');
|
||
|
|
if (result.possibility !== 0) {
|
||
|
|
fail(`cycle fabricated access: ${result.possibility}`);
|
||
|
|
}
|
||
|
|
return result;
|
||
|
|
}
|
||
|
|
|
||
|
|
const report = await rigor.campaign(
|
||
|
|
[
|
||
|
|
rigor.fn('check', check, rigor.args(
|
||
|
|
rigor.gen.object({
|
||
|
|
cycleSize: rigor.gen.int(2, 6),
|
||
|
|
memberP: rigor.gen.oneOf([0.25, 0.5, 1])
|
||
|
|
})
|
||
|
|
))
|
||
|
|
],
|
||
|
|
rigor.crucible([
|
||
|
|
rigor.invariant('cycle-safe', ({ error, errorMessage }) => !error && !errorMessage)
|
||
|
|
])
|
||
|
|
).run({ effort: 400, seed: 'zanzibar-cycle-safety' });
|
||
|
|
|
||
|
|
const inv = report.crucibleVerdict?.invariants?.find(i => i.name === 'cycle-safe');
|
||
|
|
assert.ok(inv);
|
||
|
|
assert.equal(inv.passed, true, `CYCLE SAFETY violated in ${inv.failureCount} cases`);
|
||
|
|
});
|
||
|
|
});
|