Postern

Agents need a governance layer at the lake

Agent rights are context-driven — principal, task, scope — and the same agent code may legitimately serve different views on different calls. Static identity → role → permission can't encode that; per-engine RLS doesn't survive ETL; tenant segregation forfeits cross-source joins. Policy has to move to the query plane.

flowchart LR
  classDef ok fill:#eef,stroke:#446,color:#333
  classDef agent fill:#fec,stroke:#b15c2e,color:#333
  classDef bad fill:#fee,stroke:#a33,color:#333,stroke-dasharray:4

  subgraph rbac["RBAC (stable, fits humans)"]
    direction LR
    u[user]:::ok --> rl[role]:::ok --> pm[perms]:::ok
  end

  subgraph reality["Agent (context-driven, per call)"]
    direction LR
    pr[principal]:::agent --> ag[agent]:::agent
    tk[task] -.-> ag
    sc[scope] -.-> ag
    ag --> vv{{"view varies per call"}}:::bad
  end
        

Architecture

Adapted from paper §Design (Layer 1 rewriter) and §4 (Layer 2 capability-bounded data flow).

flowchart LR
  agent[LLM agent] -->|plan + biscuit| gw{{Postern gateway}}
  subgraph TCB[trusted base]
    gw -->|sig verify| bc[biscuit-auth]
    bc -->|principal + token facts| ev["biscuit Datalog eval
(planned)"]
    pol[(policy: right facts)] --> ev
    ev -->|allow-set| rw["plan rewriter
(Lean ref ↔ Rust mirror)"]
    cat[(catalog)] --> rw
    rw -->|Option Plan| exe[DuckDB / Polars]
    exe --> guard["capability-bounded sink
Cap·Tagged · opaque receipt"]
  end
  guard -->|receipt| agent
        

Layer 1 (rewriter) constrains what data reaches the agent; Layer 2 (capability-bounded sink) constrains what the agent's code may do with released values. Rust mirror is hand-written and pinned to the Lean reference by two conformance harnesses: postern-diff (31/31 rewriter cases, Lean reference ↔ Rust impl) and postern-datalog-diff (9/9 Datalog cases, Lean Program.allowed ↔ biscuit_auth::datalog::World). Property-based differential testing is an open problem (§6).

Sample policy — financial institution

Surface syntax (left) is sugar over ground right(principal, relation, column) Datalog facts (right) — the in-scope fragment of biscuit-auth's Datalog dialect. Attenuation, expiry, audience, and key rotation are open problems (paper §6).

grant CRM       on users_data
  { id, name, region, age }

grant CardOps   on cards_data
  { card_id, card_type, limit, activated }

grant FraudRisk on transactions_data
  { txn_id, card_id, amount, merchant, timestamp }

grant FraudRisk on users_data
  { id, region }

right("CRM", "users_data", "id");
right("CRM", "users_data", "name");
right("CRM", "users_data", "region");
right("CRM", "users_data", "age");

right("CardOps", "cards_data", "card_id");
right("CardOps", "cards_data", "card_type");
…
right("FraudRisk", "users_data", "id");
right("FraudRisk", "users_data", "region");

Multiple grants on the same (p, r) flat-union — the policy language is monotone grant-only, so review is additive: a new grant can only widen. Anything outside the union is denied (fail-closed).

What Lean proves

Axioms of proven theorems are bounded by { propext, Quot.sound } — Lean 4's foundational set; no Classical.choice, no user-supplied axioms. Five residuals isolated as sorryAx in CheckAxioms.lean: three on the Join arm of Theorems 5, 6, 9; two Datalog headlines (eval_sound, eval_terminates). Eight Datalog support lemmas and the combinatorial helpers underpinning herbrandBound_mono all proved from Init stdlib, no Mathlib.

Learning from Cedar

postern-core mirrors the Lean rewriter one-for-one. The gateway evaluates policies through biscuit_auth::datalog::World behind a Cargo feature flag.

• postern-core — Plan IR, policy, rewrite().
• postern-guardrail — paper §4's capability-bounded data flow: branded Cap<'sc, C>, invariant 'sc, opaque-receipt sinks (three compile_fail doctests pin the lexical escape attempts).
• postern-diff — rewriter conformance harness, asserts Rust output is byte-equal to the Lean reference on a hand-curated JSON corpus (31/31 cases across Project, Filter(Pred), Join, Aggregate).
• postern-datalog-diff — Datalog conformance harness, asserts Lean Program.allowed mem-set-equals biscuit_auth::datalog::World on a second corpus (9/9 cases, ground facts + Horn rules).
• postern-wasm — small WASM bundle this site loads.

The gateway's native build evaluates policies through biscuit_auth::datalog::World directly (postern-core::datalog, behind the datalog-biscuit Cargo feature). The browser-side WASM bundle powering the demo still ships the column-grant DSL evaluator only — pulling biscuit-auth through wasm-bindgen would bloat the bundle, so the WASM-only migration stays on the §6 list.

Capability-bounded data flow

The rewriter constrains what data reaches the agent. A separate layer constrains what the agent's code may do with the values released. Inspired by Odersky et al.'s Scala 3 capture-checking; Rust has none, so we mechanise a weaker analog out of three pure-Rust constructions.

pub fn to_llm<'sc, T, C, S>(
    cap: Cap<'sc, C>,
    data: Tagged<'sc, T, C>,
    serialize: S,
) -> LlmAck
where S: FnOnce(T) -> String;   // T never escapes the sink

Construction is the one used by ghost-cell for branded references. Crate is no_std-compatible (paper §4).

Open problems

• Filter value-channel — the syntactic coverage condition (T13) blocks reads of forbidden columns; it does not yet model exfiltration via mutual information between allowed and forbidden values (channel-capacity / per-principal budget calculus, citing SEAL and faceted-IF).
• Join-arm residuals — three sorryAx on T5, T6, T9 over the Join arm: per-leg idempotence composition; widening through a two-leg key check; cross-leg forbidden-filter refusal.
• DP-mechanism instantiation — T12 ships an abstract aggAllowed predicate; closing it under a specific mechanism (ε-budget, Laplace, Gaussian, k-anonymity) is the next step.
• Datalog headlines — eval_sound and eval_terminates remain stated with sorryAx; both reduce to a body-grounding lemma and a finite-Herbrand pigeonhole.
• Biscuit block attenuation, audience, expiry, key rotation — verified outside the proof today; lifting them into Lean removes the principal-extraction row from the trusted base.
• WASM-side biscuit-Datalog backend (bundle-size tradeoff); property-based differential testing against the two conformance corpora.

Paper §6 enumerates the full open-problem list.

Read the paper · PDF · Try the WASM demo · GitHub