Pith. sign in

REVIEW 3 major objections 6 minor 24 references

Access-control policies become trustworthy when reviewed intent is fixed first and a verifier steers the model until the policy matches that target.

Reviewed by Pith at T0; open to challenge. T0 means a machine referee read the full paper against a public rubric. the ladder, T0–T4 →

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

T0 review · grok-4.5

2026-07-12 00:52 UTC pith:W23J37F7

load-bearing objection Solid systems paper: fixed-target authoring plus a typed repair signal for Cedar, with full-benchmark formal convergence and an honest conditional guarantee. the 3 major comments →

arxiv 2607.03656 v1 pith:W23J37F7 submitted 2026-07-04 cs.SE cs.AIcs.CR

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

Adarsh Vatsa , Sachi Shome , Yingming Zhou , William Eiers This is my paper
classification cs.SE cs.AIcs.CR
keywords access controlCedar policiesLLM synthesisverifier-guided generationpolicy authoringCEGISintent atomsauthorization boundaries
verification ladder T0 review T1 audit T2 compute T3 formal T4 reserved

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

Turning natural-language access-control requirements straight into policy code is unsafe: a model can emit something that compiles and looks right while granting access nobody approved. AutoCedar claims the real work is to complete and freeze what the requirements mean before any candidate is written, then search for Cedar that satisfies that fixed target. Requirements are broken into small intent atoms about vocabulary and behavior; after mechanical checks and human review, those atoms become a schema and a boundary of floors, ceilings, and liveness slices the model cannot rewrite. The model proposes candidates; each verifier failure becomes a directed repair signal—tighten, loosen, or expand—without changing the target. The paper shows this loop reaches formal satisfaction on every task in its 221-scenario benchmark and turns three noisy real-world requirement corpora into reviewed, globally checked Cedar policy stores.

Core claim

End-to-end access-control authoring becomes tractable when the model is confined to small problems grounded in reviewed intent and steered by verifier feedback. AutoCedar does not treat requirements as a finished specification: it surfaces gaps, completes intent into a human-approved schema and boundary plan, holds that plan outside the model’s control, and runs a counterexample-guided search in which a typed signal layer turns every failed check into a target-preserving repair instruction rather than a vague rejection.

What carries the argument

The synthesis sandwich—a boundary plan of floor policies (required access), ceiling policies (maximum approved access), and liveness slices (approved workflows that must stay nonempty)—plus the signal-layer contract that maps each verifier failure to a repair packet with direction, witness, and history without mutating the approved plan.

Load-bearing premise

The guarantee only holds if the human-approved boundary plan truly captures what the organization meant to allow and deny.

What would settle it

Find a set of authorization requests whose correct allow/deny answers are fixed independently of AutoCedar’s plan; if policies that fully pass the approved floors, ceilings, and liveness checks still systematically decide those requests wrong, the claim that plan satisfaction predicts intent-level correctness fails.

Watch this falsifier — get emailed when new claim-graph text bears on it.

If this is right

  • A returned policy can be certified against a fixed semantic boundary rather than judged only by syntax or surface plausibility.
  • Fragmented natural-language and extracted access-control fragments can be turned into deployable, globally checked Cedar policy stores.
  • Reviewed targets alone shrink residual errors; shaped repair signals close the remaining stubborn failures.
  • When requirements change, the recorded intent log can be edited and a fresh verified policy re-authored without silent drift into unapproved behavior.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The same fixed-target-plus-signal pattern likely transfers to other security-critical generation tasks where a defect is defined only relative to stated intent, not by a crash or sanitizer.
  • Independent audits of reviewer-approved atoms against production access logs would test whether human-built plans systematically under- or over-specify real organizational policy.
  • Holding the verifier fixed while removing or degrading human target review would quantify how much reported success comes from careful intent construction versus search.
  • Benchmarks for LLM policy tools should measure global boundary satisfaction and cross-rule interference, not isolated snippet plausibility.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit.

Referee Report

3 major / 6 minor

Summary. AutoCedar is a verifier-guided authoring loop that first turns natural-language access-control requirements into a human-reviewed Cedar schema and boundary plan Π = (C, F, G) of ceilings, floors, and liveness slices, then synthesizes Cedar policy candidates under a CEGIS-style discipline in which cedar symcc owns accept/reject and a typed signal layer Φ maps failures to target-preserving repair directions (TIGHTEN/LOOSEN/EXPAND/LOCAL). The paper contributes the intent-atom review model, the signal-layer contract (Table I, Alg. 2), CedarBench (221 executable tasks), and three ACRE/REDE-derived case studies. Empirically, AutoCedar converges on 221/221 CedarBench scenarios (Table II), ablations show residual loss falling from 15.58 (schema-only) to 0.00 (full signal stack) on a 100-scenario slice (Table III), and Category-2 baselines lag on full property pass rates (Table V: 100% vs 79.6%/1.4%). Proposition 1 states conditional soundness: returned policies are certified against the approved plan, not against organizational intent in the abstract.

Significance. If the scoped claim holds, the work is a substantial contribution to secure LLM-assisted policy authoring: it separates intent completion from code generation, makes the authorization boundary an explicit, fixed oracle, and supplies a reusable repair interface between symbolic policy evidence and a stochastic proposer. Strengths that should be credited include (i) machine-checked inclusion/liveness via cedar symcc rather than test-suite proxies, (ii) full 221/221 formal convergence with open implementation and benchmarks, (iii) a clean ablation isolating reviewed targets vs. shaped repair signals (Table III), and (iv) honest conditional soundness (Prop. 1) and threats (§VI). The problem is timely given OWASP ranking of broken access control and rising AI-authored authorization logic. The main significance is methodological: a boundary-preserving authoring loop that other security-sensitive synthesis settings can reuse.

major comments (3)
  1. [§V.D RQ3; Table VI] §V.D (RQ3) and Table VI: the claim that satisfying AutoCedar’s verification plan “reliably predict[s] policy correctness with respect to NL intent” is only weakly supported. Semantic request sets are author-constructed from the same NL under the AutoCedar schema, so property checks and request matches share a single interpretive pipeline rather than providing independent NL-level ground truth. Please either (a) obtain independent annotator-built request oracles, or (b) reframe RQ3 as consistency between plan satisfaction and author-derived request tests, not as external prediction of organizational intent.
  2. [Abstract; §I Contributions; §V; §VI] Abstract, Contributions item 4, and §V case studies: the end-to-end claim that AutoCedar “converts noisy prose … into … a globally verified Cedar policy store” for healthcare/education/conference scenarios depends on boundary plans constructed for this study (§VI). That is a legitimate evaluation design, but the abstract and contribution list currently read as if the targets were independently given. Scope the claim explicitly to author-reviewed (or simulated-review) plans, and report how much of the external-corpus plan was human-edited vs. model-proposed before admission.
  3. [§V.C Table III] §V.C Table III: the signal-layer ablation is reported only on a fixed 100-scenario slice, while the headline result is 221/221. Residual-loss and convergence gaps between “native verifier loop” (94/100, loss 0.10) and “full signal stack” (100/100, loss 0.00) are load-bearing for the signal-layer contribution claim. Either run the same four conditions on all 221 tasks or justify that the 100-scenario slice is representative (domain coverage, difficulty, mutation vs. hand-authored mix) so the last-six-failures result generalizes.
minor comments (6)
  1. [§V.D Figures 3–4] Figure 3 and Figure 4 are referenced as error-profile and domain heatmaps but are hard to interpret from the text alone; add axis units, sample sizes per domain, and a short caption note on how “fully-correct rate” is computed.
  2. [§III.A Algorithm 1] Algorithm 1 line 11 initializes m as a “summary of the fixed target”; clarify whether this summary is a fixed template, an LLM-generated digest, or the full Π encoding, since that choice affects reproducibility of iteration-1 proposals.
  3. [§V.A–B Table II] §V.A: report variance or per-scenario iteration histograms for Table II (means only), and state temperature/sampling settings for GPT-5.5 low and Haiku 4.5.
  4. [§V.D.3] Human study (§V.D.3): 14 participants and 98 probes is useful preference evidence but sparse on live HITL; move stronger wording about “readers more often judged” into a clearly labeled exploratory subsection and note non-expert vs. security-engineer composition if available.
  5. [§I] Minor polish: consistent spacing around AUTOCEDAR (sometimes “AUTOCEDAR,” sometimes “AUTOCEDAR ”), and fix “OW ASP” → “OWASP” in the introduction.
  6. [§VII] Related work could briefly position against recent policy-as-code / Cedar tooling and against LLM-based configuration repair outside access control, to help non-Cedar readers place the signal-layer contribution.

Circularity Check

0 steps flagged

No significant circularity: formal acceptance is independent cedar-symcc checking against a fixed reviewed plan; evaluation-scope limits are stated, not smuggled.

full rationale

AutoCedar’s load-bearing technical claim is a CEGIS-style loop: once a human-approved schema Σ and boundary plan Π = (C, F, G) are fixed, an LLM proposes candidates and cedar symcc (with cvc5) independently certifies floor inclusion, ceiling inclusion, and liveness (Theorem 1, Prop. 1, Alg. 1–2). That accept/reject decision is not defined in terms of the model’s proposal and is not a fit renamed as a prediction. Self-citations [4],[5] supply motivation (prior semantic-equivalence rates for direct LLM policy generation), not a uniqueness theorem or ansatz that forces the present method. CedarBench and the three corpus plans are author-constructed evaluation substrates, and Prop. 1 / §VI explicitly condition organizational-intent validity on human plan fidelity—so measured “correctness” is relative to reviewed targets by design, not by a hidden reduction of Eq. X to Eq. Y. That is a scope/validity limit the paper owns, not circular derivation. Score 1 only for the mild, acknowledged evaluation self-grounding; the synthesis and verification chain itself is self-contained against an external symbolic checker.

Axiom & Free-Parameter Ledger

2 free parameters · 4 axioms · 4 invented entities

The central empirical claim rests on Cedar's typed deny-overrides semantics and symbolic comparison, on human (or simulated) approval of intent atoms as the source of organizational truth, and on evaluation targets that are either benchmark-authored or study-constructed. Free parameters are operational (iteration budget, model choice), not fitted physical constants. Invented entities are engineering constructs (atoms, boundary plan, signal layer, CedarBench) with independent handles via the open verifier and released artifacts, not unfalsifiable physical mediators.

free parameters (2)
  • iteration budget K = 20 (CedarBench driver)
    Search is capped (reported driver uses 20 iterations); convergence claims are within this budget, not unbounded completeness.
  • proposer model choice and sampling = GPT-5.5 low; Haiku 4.5
    Results depend on GPT-5.5 low and Haiku 4.5 configurations; LLM nondeterminism is acknowledged and partially handled via Pass@1/Pass@3 for baselines.
axioms (4)
  • domain assumption Cedar deny-overrides permit-set semantics and schema-typed request universe R_Σ are the correct behavioral denotation for comparing policies.
    Background §II; all floors/ceilings/liveness are defined via sem(P).
  • domain assumption cedar symcc + SMT (cvc5) correctly decides inclusion/equivalence/witnesses over the supported Cedar fragment used in checks.
    Used as oracle throughout §III–V; lineage cited via Zelkova.
  • domain assumption Human intent review of plain-English atoms accurately captures organizational authorization intent for the approved plan Π.
    Prop. 1 and §III.C explicitly make all semantic guarantees relative to this assumption.
  • ad hoc to paper Benchmark and study-constructed boundary plans are fair executable stand-ins for measuring synthesis against reviewed intent.
    §IV–VI: CedarBench plans are artifacts; external-corpus plans constructed for evaluation, not independently audited production policies.
invented entities (4)
  • Intent atoms (schema atoms + property atoms) with dual mechanical/intent status independent evidence
    purpose: Decompose requirements into reviewable vocabulary and behavior claims that compile into Σ and Π.
    Core intermediate representation of AutoCedar (§III.C); engineering construct, not a physical entity.
  • Boundary plan Π = (C, F, G) floors/ceilings/liveness sandwich independent evidence
    purpose: Make acceptable authorization behavior checkable without requiring a single golden policy encoding.
    Def. 1 / Thm. 1; falsifiable via symbolic inclusion and liveness checks.
  • Signal layer Φ with typed repair packets (TIGHTEN/LOOSEN/EXPAND/LOCAL) independent evidence
    purpose: Translate verifier evidence into target-preserving model-facing repair without rewriting the oracle.
    §III.D, Alg. 2, Table I; evaluated by ablation residual loss.
  • CedarBench (221 executable semantic-boundary tasks) independent evidence
    purpose: Measure fixed-target verifier-guided synthesis rather than isolated NL-to-syntax translation.
    §IV contribution; released as evaluation substrate.

pith-pipeline@v1.1.0-grok45 · 21038 in / 3591 out tokens · 31944 ms · 2026-07-12T00:52:35.942068+00:00 · methodology

0 comments
read the original abstract

Large Language Models are increasingly used to turn natural-language requirements into code. In access control, that shortcut is dangerous: a generated policy can compile and read correctly while granting access that no one approved. The difficulty is not only writing policy code. It is fixing what the requirements mean before code is written, and then checking that the final policy actually satisfies that intent. We present AutoCedar, a verifier-guided system that first turns natural-language access-control requirements into a reviewed, checkable target, and then synthesizes Cedar policies against that target. AutoCedar decomposes schema and policy authoring into small intent atoms: reviewable claims about vocabulary and behavior. Once those atoms pass mechanical validation and human intent review, the model proposes a candidate policy, the verifier checks it against the approved target, and each failure is turned into a repair signal that tells the model whether to broaden, narrow, or restructure the policy without changing the target. Because the model's work is split into small problems, each grounded in reviewed intent and backed by verifier feedback, end-to-end policy authoring becomes tractable. AutoCedar converges on all 221 tasks of CedarBench, our benchmark of authorization tasks paired with executable semantic boundaries. Across three requirements-corpus case studies covering healthcare, education, and conference management, AutoCedar converts noisy prose and extracted access-control fragments into reviewed schemas, formal checks, and a globally verified Cedar policy store for each scenario.

Figures

Figures reproduced from arXiv: 2607.03656 by Adarsh Vatsa, Sachi Shome, William Eiers, Yingming Zhou.

Figure 1
Figure 1. Figure 1: AUTOCEDAR as fixed-target construction plus verifier-guided search. Raw requirements D are indexed into a source DAG GD: stable source nodes and bounded context packets used to propose atoms. A is the set of approved schema and property atoms, Σ is the Cedar schema, Π is the boundary plan, and F, C, G are the approved floors, ceilings, and liveness slices. Some review-level constraints are derived: they ar… view at source ↗
Figure 2
Figure 2. Figure 2: The synthesis sandwich. The dashed rectangle is an intermediate [PITH_FULL_IMAGE:figures/full_fig_p004_2.png] view at source ↗
Figure 3
Figure 3. Figure 3: Error profile of validation-passing policies on CedarBench [PITH_FULL_IMAGE:figures/full_fig_p008_3.png] view at source ↗
Figure 4
Figure 4. Figure 4: Fully-correct rate (%) across CedarBench’s domains. Each cell is the [PITH_FULL_IMAGE:figures/full_fig_p009_4.png] view at source ↗

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

24 extracted references · 9 linked inside Pith

  1. [1]

    A01 Broken Access Control – OW ASP Top 10:2025,

    OW ASP Foundation, “A01 Broken Access Control – OW ASP Top 10:2025,” OW ASP Top 10:2025, 2025, accessed: 2026-06-28

    2025

  2. [2]

    Sonar Data Reveals Critical “Verification Gap

    SonarSource, “Sonar Data Reveals Critical “Verification Gap” in AI Coding,” SonarSource press release, 2026, accessed: 2026-06-28

    2026

  3. [3]

    Project Glasswing: An Initial Update,

    Anthropic, “Project Glasswing: An Initial Update,” Anthropic research update, 2026, accessed: 2026-06-28

    2026

  4. [4]

    Synthesizing access control policies using large language models,

    A. Vatsa, P. Patel, and W. Eiers, “Synthesizing access control policies using large language models,” inProceedings of the 4th International Workshop on Natural Language-Based Software Engineering, 2025, arXiv:2503.11573

    Pith/arXiv arXiv 2025

  5. [5]

    Exploring large language models for access control policy synthesis and summarization,

    A. Vatsa, B. Hall, and W. Eiers, “Exploring large language models for access control policy synthesis and summarization,”arXiv preprint arXiv:2510.20692, 2025

    Pith/arXiv arXiv 2025

  6. [6]

    Cedar: A new lan- guage for expressive, fast, safe, and analyzable authorization (extended version),

    J. W. Cutler, C. Disselkoen, A. Eline, S. He, K. Headley, M. Hicks, K. Hietala, E. Ioannidis, J. Kastner, A. Mamat, D. McAdams, M. Mc- Cutchen, N. Rungta, E. Torlak, and A. M. Wells, “Cedar: A new lan- guage for expressive, fast, safe, and analyzable authorization (extended version),”arXiv preprint arXiv:2403.04651, 2024

    Pith/arXiv arXiv 2024

  7. [7]

    Cedar policy language,

    “Cedar policy language,” cedarpolicy.com, accessed: 2026-06-24

    2026

  8. [8]

    Semantic-based automated reasoning for AWS access policies using SMT,

    J. Backes, P. Bolignano, B. Cook, C. Dodge, A. Gacek, K. Luckow, N. Rungta, O. Tkachu, and C. Varming, “Semantic-based automated reasoning for AWS access policies using SMT,” inProceedings of the 18th Conference on Formal Methods in Computer-Aided Design, 2018, pp. 1–9

    2018

  9. [9]

    Access control policy extraction from unconstrained natural language text,

    J. Slankas and L. Williams, “Access control policy extraction from unconstrained natural language text,” inProceedings of the 2013 Inter- national Conference on Social Computing. IEEE, 2013, pp. 435–440

    2013

  10. [10]

    Relation extraction for inferring access control rules from natural language artifacts,

    J. Slankas, X. Xiao, L. Williams, and T. Xie, “Relation extraction for inferring access control rules from natural language artifacts,” inPro- ceedings of the 30th Annual Computer Security Applications Conference. ACM, 2014, pp. 366–375

    2014

  11. [11]

    cvc5: A versatile and industrial-strength SMT solver,

    H. Barbosa, C. W. Barrett, M. Brain, G. Kremer, H. Lachnitt, M. Mann, A. Mohamed, M. Mohamed, A. Niemetz, A. N ¨otzli, A. Ozdemir, M. Preiner, A. Reynolds, Y . Sheng, C. Tinelli, and Y . Zohar, “cvc5: A versatile and industrial-strength SMT solver,” inTools and Algorithms for the Construction and Analysis of Systems, ser. Lecture Notes in Computer Science...

    2022

  12. [12]

    Program synthesis by sketching,

    A. Solar-Lezama, “Program synthesis by sketching,” Ph.D. dissertation, University of California, Berkeley, December 2008. [Online]. Available: https://www2.eecs.berkeley.edu/Pubs/TechRpts/ 2008/EECS-2008-177.html

    2008

  13. [13]

    Coun- terexample guided inductive synthesis modulo theories,

    A. Abate, C. David, P. Kesseli, D. Kroening, and E. Polgreen, “Coun- terexample guided inductive synthesis modulo theories,” inComputer Aided Verification. Springer, 2018, pp. 270–288

    2018

  14. [14]

    Generative language modeling for automated theorem proving,

    S. Polu and I. Sutskever, “Generative language modeling for automated theorem proving,”arXiv preprint arXiv:2009.03393, 2020

    Pith/arXiv arXiv 2009

  15. [15]

    Draft, sketch, and prove: Guiding formal theorem provers with informal proofs,

    A. Q. Jiang, S. Welleck, J. P. Zhou, T. Lacroix, J. Liu, W. Li, M. Jamnik, G. Lample, and Y . Wu, “Draft, sketch, and prove: Guiding formal theorem provers with informal proofs,” inInternational Conference on Learning Representations, 2023

    2023

  16. [16]

    Baldur: Whole-proof generation and repair with large language models,

    E. First, M. N. Rabe, T. Ringer, and Y . Brun, “Baldur: Whole-proof generation and repair with large language models,” inProceedings of the 31st ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering, 2023, pp. 1229–1241

    2023

  17. [17]

    Hilbert: Recursively building formal proofs with informal reasoning,

    S. Varambally, T. V oice, Y . Sun, Z. Chen, R. Yu, and K. Ye, “Hilbert: Recursively building formal proofs with informal reasoning,”arXiv preprint arXiv:2509.22819, 2025

    arXiv 2025

  18. [18]

    LEAP: Supercharging LLMs for formal mathematics with agentic frameworks,

    P.-N. Kung, L. Song, D. Hwang, J. Yoon, C.-L. Li, S. Severini, M. Olsak, E. Lockhart, Q. V . Le, B. Gokturk, T. Luong, T. Pfister, and N. Peng, “LEAP: Supercharging LLMs for formal mathematics with agentic frameworks,”arXiv preprint arXiv:2606.03303, 2026

    Pith/arXiv arXiv 2026

  19. [19]

    Thor: Wielding hammers to integrate language models and automated theorem provers,

    A. Q. Jiang, W. Li, S. Tworkowski, K. Czechowski, T. Odrzyg ´o´zd´z, P. Miło´s, Y . Wu, and M. Jamnik, “Thor: Wielding hammers to integrate language models and automated theorem provers,” inAdvances in Neural Information Processing Systems, 2022. [Online]. Available: https://arxiv.org/abs/2205.10893

    Pith/arXiv arXiv 2022

  20. [20]

    LeanDojo: Theorem proving with retrieval-augmented language models,

    K. Yang, A. M. Swope, A. Gu, R. Chalamala, P. Song, S. Yu, S. Godil, R. Prenger, and A. Anandkumar, “LeanDojo: Theorem proving with retrieval-augmented language models,” inAdvances in Neural Information Processing Systems, 2023. [Online]. Available: https://arxiv.org/abs/2306.15626

    Pith/arXiv arXiv 2023

  21. [21]

    DeepSeek-Prover-V1.5: Harnessing proof assistant feedback for reinforcement learning and monte-carlo tree search,

    H. Xin, Z. Z. Ren, J. Song, Z. Shao, W. Zhao, H. Wang, B. Liu, L. Zhang, X. Lu, Q. Du, W. Gao, Q. Zhu, D. Yang, Z. Gou, Z. F. Wu, F. Luo, and C. Ruan, “DeepSeek-Prover-V1.5: Harnessing proof assistant feedback for reinforcement learning and monte-carlo tree search,”arXiv preprint arXiv:2408.08152, 2024. [Online]. Available: https://arxiv.org/abs/2408.08152

    Pith/arXiv arXiv 2024

  22. [22]

    Faithful autoformalization via roundtrip verification and repair,

    D. Amrollahi, J. Lopez, and C. Barrett, “Faithful autoformalization via roundtrip verification and repair,”arXiv preprint arXiv:2604.25031, 2026

    Pith/arXiv arXiv 2026

  23. [23]

    Quantifying permissiveness of access control policies,

    W. Eiers, G. Sankaran, A. Li, E. O’Mahony, B. Prince, and T. Bultan, “Quantifying permissiveness of access control policies,” inProceedings of the 44th International Conference on Software Engineering, 2022, pp. 1805–1817

    2022

  24. [24]

    Quantitative policy repair for access control on the cloud,

    W. Eiers, G. Sankaran, and T. Bultan, “Quantitative policy repair for access control on the cloud,” inProceedings of the 32nd ACM SIGSOFT International Symposium on Software Testing and Analysis, 2023, pp. 564–575

    2023