AutoCedar: An Agentic Framework for Verifier-Guided Access Control Policy Synthesis¶

🕒 Published (v1): 2026-07-04 01:13 UTC · Source: Arxiv · link

Why this paper was selected

Verifier-guided agentic synthesis; novel safety pattern for harnesses in high-stakes domains

Ask a follow-up

Open an assistant pre-loaded with this paper's context.

TL;DR¶

AutoCedar is a verifier-guided agentic framework that converts natural-language access-control requirements into formally verified Cedar policies by first constructing a reviewed semantic boundary (floors, ceilings, liveness slices) and then running a CEGIS-style LLM-proposer/verifier loop against that fixed target. The key insight is that the LLM must never be allowed to modify the target; it only proposes candidates while a signal layer translates verifier failures into typed repair packets. AutoCedar achieves 100% convergence on CedarBench (221 tasks) and three real-world requirements corpora.

Problem¶

Direct LLM-to-policy translation produces syntactically valid but semantically incorrect policies with no internal correctness signal — prior work reports only 45.8%–93.7% semantic equivalence against ground truth. Worse, natural-language requirements are typically incomplete: pairing an LLM with a verifier is insufficient if the target specification itself has gaps, since verification against an under-specified intent cannot detect missing cases. There is no principled method to turn noisy prose into a deployed, globally-checked policy store.

Method¶

AutoCedar decomposes synthesis into two strictly ordered phases:

Phase 1 — Target construction. Requirements document $D$ is indexed into a source DAG $G_D$. The system proposes schema atoms (entity types, actions, attributes) and property atoms (behavioral constraints) one bounded source packet at a time. Each atom $a = (s, k, u, z, \sigma_\text{sym}, \sigma_\text{intent})$ must pass both mechanical validation ($\sigma_\text{sym}$) and human intent review ($\sigma_\text{intent}$) before entering the approved set $A$. Approved atoms compile into a Cedar schema $\Sigma$ and a boundary plan $\Pi = (C, F, G)$: ceiling policies $C$ (maximum permitted access), floor policies $F$ (required access), and liveness slices $G$ (workflow classes that must remain non-empty). If a property atom requires schema support that does not yet exist, schema repair reruns before the property is shown to the reviewer. The target is fixed only after coverage accounting and admission checks (schema validation, pairwise floor-vs-ceiling checks, liveness/probe checks) pass.

Phase 2 — Verifier-guided candidate search. Given fixed $\Pi$, the LLM proposes candidate bundles $P_t$. The verifier uses cedar-symcc (SMT-based symbolic comparison) to check the synthesis sandwich: $$L_\Pi \subseteq \text{sem}(P_t) \subseteq U_\Pi \quad\text{and}\quad \forall G_k \in G.\; \text{sem}(P_t) \cap G_k \neq \emptyset$$ where $L_\Pi = \bigcup_{F_j} \text{sem}(F_j)$ and $U_\Pi = \bigcap_{C_i} \text{sem}(C_i)$. Failures are classified by a signal layer $\Phi(Q_t, P_t, \Pi, H_t) \to m_{t+1}$ into four typed obligation classes (Table I): target admission (O1), semantic direction — TIGHTEN/LOOSEN/EXPAND (O2), local Cedar diagnostics (O3), and history/non-progress detection (O4). Each repair packet carries only evidence that preserves the approved target; the signal layer is explicitly prohibited from mutating $\Pi$, inverting polarity, or inventing witnesses.

Key Contributions¶

AutoCedar — the full verifier-guided authoring loop: intent atoms → reviewed schema and boundary plan → CEGIS-style LLM synthesis
Boundary plan formalism — $\Pi = (C, F, G)$ with formal plan satisfaction (Definition 1) and the synthesis sandwich theorem (Theorem 1) as the verifier's acceptance condition
Signal-layer contract — four typed obligation classes (O1–O4) that translate cedar-symcc evidence into target-preserving repair packets without model control over the target
CedarBench — 221-scenario verification benchmark plus three ACRE/REDE-derived case studies (healthcare, education, conference management) for end-to-end evaluation

Results¶

AutoCedar converges on all 221 tasks of CedarBench (100% convergence rate)
Across three real-world requirements corpora (healthcare, education, conference management), noisy NL prose and extracted NLACP fragments are transformed into globally verified Cedar policy stores
Baseline comparison: direct LLM roundtrip generation achieves 45.8% semantic equivalence (non-reasoning models) and 93.7% (reasoning models) — cited from prior work as the motivation, not a direct experimental comparison within this paper

Limitations¶

Conditional soundness only: the semantic guarantee holds relative to the human-approved plan $\Pi$; if reviewers approve an incorrect boundary, the synthesized policy inherits that error
No claim of solving a complete global feasibility problem — admission checks are pairwise and probe-based, not a full SMT check over the entire plan
A compatible plan may still lack a concise Cedar implementation, or the model may fail to find one within the iteration budget $K$
CedarBench uses simulated review as a measurement instrument; this does not confer intent authority — the correctness claim is conditioned on real human review
Rate-limit-style atoms contribute only through the finite verifier obligations AutoCedar can compile from them; runtime enforcement outside Cedar's semantics is out of scope
Evaluation is limited to the Cedar policy language; generalization to other declarative policy languages (e.g., OPA/Rego, AWS IAM) is undemonstrated

Relevance to Harnesses / Meta-Harnesses¶

AutoCedar is a concrete example of a structured agentic harness: it orchestrates an LLM proposer, a formal verifier, and a human reviewer through a deterministic control-flow loop (Algorithm 1) with typed inter-component contracts. The signal layer $\Phi$ is precisely the kind of adapter that meta-harness designers must build — translating one subsystem's output format (SMT counterexamples) into structured inputs for another (the LLM repair prompt) without leaking unreviewed state across the boundary. The pattern of fixing the target outside model control before entering the generation loop is a generalizable harness design principle: the LLM operates only within a reviewed, immutable specification, and the harness owns accept/reject authority. This connects directly to the broader line of work on CEGIS-style synthesis harnesses and to emerging frameworks that separate "oracle" from "proposer" roles in LLM pipelines.