Postern

Agents need a governance layer at the lake

An agent's effective rights are context-driven: which principal it acts for, which task it was invoked under, which scope the caller granted. The same agent code, called by two principals — or by one principal under two tasks — must read two different views.

Traditional RBAC bakes a static identity → role → permission chain at provisioning time and cannot encode any of those axes. Per-engine RLS doesn't survive the ETL boundary; tenant segregation forfeits the cross-source joins that motivate the lakehouse. Policy has to move to the query plane, gated under the agent's task-scoped identity at query time.

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] -->|MCP plan + biscuit| gw{{Postern gateway}}
  subgraph TCB[trusted base]
    gw -->|verify| bc[biscuit verifier]
    bc -->|principal| rw["plan rewriter
(Lean ref ↔ Rust mirror)"]
    pol[(policy)] --> rw
    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 the postern-diff conformance harness (18/18 cases); property-based differential testing is an open problem (§6).

What Lean proves

Axioms of proven theorems: { propext, Quot.sound }. eval_monotone's body is written but reduces to herbrandBound_mono — a labelled sorry we expose rather than hide. Eight supporting iterator lemmas are proven.

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 — reference-conformance harness, asserts Rust output is byte-equal to the Lean reference on a hand-curated JSON corpus (18/18 cases: 15 accept, 3 refuse).
• postern-wasm — surface this site loads.

The WASM module powering the demo is today the column-grant DSL evaluator; Biscuit-Datalog migration in progress.

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

• Block attenuation — biscuit blocks can shrink rights mid-flight; the rewriter doesn't yet model this.
• Audience checks + expiry — bind tokens to gateway identity and a time window.
• Key rotation for the verifier without invalidating in-flight tokens.
• Cross-relation joins — the current IR is single-relation; multi-relation grants compose non-trivially.
• Aggregation with a DP boundary — summary outputs without leaking row-level columns.

Paper §6 enumerates the full open-problem list.

Read the paper · Try the WASM demo · GitHub