Property-Based Testing for Tenant Isolation

Enumerated tests cover the sequences someone imagined; property-based tests cover the ones nobody did, which is where isolation bugs actually live. This page is a focused part of Cross-Tenant Leak Detection & Testing: modelling the operation space, expressing the invariant, and turning each counterexample into a permanent regression test.

Problem Framing

Isolation bugs are rarely in a single operation. GET /documents is easy to test and usually correct. The bugs appear in transitions: a document shared with a second tenant and then unshared, a user moved between workspaces while a link remains, an export started before a revocation and completed after it. Each involves several operations in a particular order, and the space of orders grows factorially, so enumerating them is hopeless.

Property-based testing turns that around. Instead of enumerating sequences, generate them: pick random operations over a small set of tenants, apply them to the system, and after each one assert a single invariant that must hold universally — a read as tenant X returns only rows owned by X. When the invariant breaks, the framework shrinks the failing sequence to a minimal counterexample, which is usually two or three operations long and immediately understandable.

The value is concentrated in the shrinking. A random failure of forty operations is unusable; the same failure shrunk to "share, revoke, read" is a bug report with a fix attached.

Step-by-Step Guide

1. Model the operations, not the implementation

// model.ts
type TenantId = 'A' | 'B' | 'C';

export type Op =
  | { kind: 'createDoc';  tenant: TenantId; docId: string }
  | { kind: 'share';      tenant: TenantId; docId: string; withTenant: TenantId }
  | { kind: 'revoke';     tenant: TenantId; docId: string; fromTenant: TenantId }
  | { kind: 'moveUser';   user: string; from: TenantId; to: TenantId }
  | { kind: 'export';     tenant: TenantId }
  | { kind: 'read';       tenant: TenantId };

Keep the tenant set tiny — three is enough for every interesting interaction and keeps the state space small enough to shrink quickly. Twenty tenants makes generation slower and counterexamples harder to read without finding anything new.

2. Maintain a reference model alongside the system

// reference.ts — a deliberately naive model of who should see what
export class Reference {
  private owner = new Map<string, TenantId>();
  private shared = new Map<string, Set<TenantId>>();

  apply(op: Op) {
    switch (op.kind) {
      case 'createDoc': this.owner.set(op.docId, op.tenant); break;
      case 'share':     this.set(op.docId).add(op.withTenant); break;
      case 'revoke':    this.set(op.docId).delete(op.fromTenant); break;
      case 'moveUser':  /* membership does not change document ownership */ break;
    }
  }
  visibleTo(t: TenantId): Set<string> {
    const out = new Set<string>();
    for (const [doc, own] of this.owner) {
      if (own === t || this.set(doc).has(t)) out.add(doc);
    }
    return out;
  }
  private set(doc: string) {
    if (!this.shared.has(doc)) this.shared.set(doc, new Set());
    return this.shared.get(doc)!;
  }
}

The reference must be simple enough to be obviously correct by inspection. If it needs its own tests, it has become a second implementation and will agree with the first one's bugs.

3. Express the invariant as one assertion

// isolation.property.ts
import fc from 'fast-check';

const arbOp: fc.Arbitrary<Op> = fc.oneof(
  fc.record({ kind: fc.constant('createDoc' as const), tenant: arbTenant, docId: arbDocId }),
  fc.record({ kind: fc.constant('share' as const), tenant: arbTenant, docId: arbDocId, withTenant: arbTenant }),
  fc.record({ kind: fc.constant('revoke' as const), tenant: arbTenant, docId: arbDocId, fromTenant: arbTenant }),
  fc.record({ kind: fc.constant('read' as const), tenant: arbTenant }),
);

it('never returns a document the tenant may not see', async () => {
  await fc.assert(
    fc.asyncProperty(fc.array(arbOp, { minLength: 1, maxLength: 40 }), async (ops) => {
      await resetSystem();
      const ref = new Reference();
      for (const op of ops) {
        await applyToSystem(op);
        ref.apply(op);
        for (const t of ['A', 'B', 'C'] as const) {
          const actual = new Set(await listDocsAs(t));
          const allowed = ref.visibleTo(t);
          for (const id of actual) {
            expect(allowed.has(id)).toBe(true);      // the one invariant that matters
          }
        }
      }
    }),
    { numRuns: 200, seed: Number(process.env.PBT_SEED ?? 42), verbose: true },
  );
});

Asserting only that nothing extra is visible — rather than exact set equality — keeps the property focused on isolation. Missing rows are a functional bug worth a different test; extra rows are a security bug.

4. Fix the seed in CI and randomise nightly

{
  "scripts": {
    "test:pbt": "PBT_SEED=42 PBT_RUNS=200 vitest run isolation.property",
    "test:pbt:nightly": "PBT_SEED=$RANDOM PBT_RUNS=5000 vitest run isolation.property"
  }
}

A fixed seed in pull-request CI keeps the signal deterministic — a red build always means this change broke something. A random seed with a much higher run count nightly is what explores new territory, and any failure there becomes a new fixed regression test.

5. Promote every counterexample to an enumerated test

// regressions.spec.ts — grown from real property failures, kept forever
it('revoking a share invalidates the cached access entry (found by PBT, seed 91773)', async () => {
  await asTenant('A').post('/docs', { id: 'doc1' });
  await asTenant('A').post('/docs/doc1/share', { withTenant: 'B' });
  await asTenant('B').get('/docs/doc1').expect(200);        // warms the access cache
  await asTenant('A').delete('/docs/doc1/share/B');
  await asTenant('B').get('/docs/doc1').expect(404);        // previously returned 200
});

The property test proves the class of bug is gone; the enumerated test proves this specific one never returns, and it runs in milliseconds on every commit.

Verification

The critical question about any property test is whether it can fail at all. Verify by mutation: break isolation deliberately and confirm the property catches it.

// mutation.spec.ts — run against a build with a deliberately broken predicate
it('property fails when the tenant predicate is removed', async () => {
  process.env.MUTATION = 'drop-tenant-predicate';
  await expect(runIsolationProperty({ numRuns: 50 })).rejects.toThrow(/Property failed/);
});

it('property fails when the access cache is not invalidated on revoke', async () => {
  process.env.MUTATION = 'skip-cache-invalidation';
  await expect(runIsolationProperty({ numRuns: 200 })).rejects.toThrow(/Property failed/);
});
# Track how many runs are typically needed to find each seeded mutation.
# A mutation that needs 4,000 runs tells you the nightly budget is doing real work.
PBT_RUNS=10000 MUTATION=skip-cache-invalidation npm run test:pbt -- --reporter=json \
  | jq '.testResults[].failureMessage' | grep -o 'counterexample after [0-9]* runs'

Mutation testing is what separates a property suite that provides assurance from one that provides comfort. If deleting the tenant predicate does not turn the suite red within a handful of runs, the generator is not producing the shapes that matter.

Failure Modes & Gotchas

FAQ

How many runs are enough? A couple of hundred per pull request keeps the feedback loop fast and catches regressions in known-shaky areas. The exploration budget — several thousand runs nightly — is where new bugs come from, and the seeded-mutation measurements above are how you size it: if the hardest mutation you care about needs four thousand runs, a nightly budget of five thousand is defensible and two hundred is theatre.

Should the property run against a real database? Yes. Most isolation bugs live in the interaction between the query layer, the cache, and Row-Level Security, and none of that exists against an in-memory fake. Use a real database in a container, reset with a fast truncate between cases, and connect as the unprivileged application role so policies are actually enforced — the same discipline as in testing RLS policies for tenant isolation.

Can this find concurrency bugs? Only if the generator produces concurrency. Sequential operation lists will not find a shared batch loader or a leaked connection setting. Extend the model with a parallel step — a set of operations issued simultaneously — and accept that shrinking becomes less reliable for those cases. Many teams keep sequential property tests for logic bugs and a separate interleaved load harness for shared-state bugs, because the two need different tooling.

How long should a property suite be allowed to run before it is considered too slow? For pull-request runs, anything past three or four minutes starts changing behaviour — people begin skipping it, or the suite gets quietly reduced. The lever is case count rather than case complexity, so keep the per-run budget fixed and move exploration to the nightly job. Speeding up the reset between cases usually buys more than anything else: a truncate is far cheaper than a schema rebuild, and it is often the dominant cost in a property run against a real database.

Should the generator be biased toward operations that have previously found bugs? Mildly, and only as a supplement. Weighting share and revoke more heavily than plain reads finds state-transition bugs faster, but over-tuning the generator toward known failures narrows exploration to the space you already understand — which is the opposite of the point. Keep the weighting gentle and let the nightly run use a flatter distribution.