{"id":"d7c9ac9a-f60a-449f-bdb4-b4563164ea0a","arxiv_id":"2607.03656","paper_version":1,"verdict":"CONDITIONAL","confidence":"HIGH","novelty_score":6.5,"correctness_risk":"medium","formal_verification":"none","parameter_count":2,"one_line_summary":"AutoCedar first builds a reviewed, checkable authorization boundary from natural-language requirements, then synthesizes Cedar policies against that fixed target with verifier-guided repair, solving all 221 CedarBench tasks.","lead":"AutoCedar turns messy natural-language access rules into Cedar policies that a formal checker can prove stay inside a human-reviewed boundary. It matters because AI-written authorization code can look right while granting unapproved access, and ordinary bug-finders rarely catch that class of failure.","discovery_kind":"new_method","skeptic_critique":{"model":"grok-4.5","headline":"No significant objection identified beyond the paper's own conditional framing of intent fidelity.","rationale":"The paper's central contribution is a fixed-target, verifier-owned synthesis loop with typed repair signals, not a claim that review automatically recovers ground-truth organizational intent. Prop. 1 and §VI already fence the guarantee: semantic validity is relative to the approved plan; intent correspondence is a human judgment. CedarBench and the three case studies measure exactly that scoped claim (Tables II–VI; Figs. 3–4). The reader's CONDITIONAL/HIGH posture correctly treats review/target fidelity as the weakest premise without over-penalizing a systems result that is explicit about it. No independent load-bearing attack (e.g., that cedar symcc does not certify the sandwich, or that signal-layer direction is inverted) is supported by the text. Therefore the verdict should stay CONDITIONAL; agreement with the reader is full on the load-bearing point.","tokens_in":16973,"tokens_out":518,"duration_ms":5361,"concrete_test":"Independently re-run the full 221 CedarBench suite from the public repo with a fixed seed and the same GPT-5.5-low / Haiku configs; confirm 221/221 convergence and zero residual loss under the checked-in plans. Separately, have a non-author reviewer re-approve atoms for one external corpus (e.g., iTrust) from source only; re-synthesize and check whether property/request pass rates remain 100% under the new plan.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The reader's weakest assumption is already the paper's explicit premise (Prop. 1; Threats §VI): returned policies are certified only against human-approved plans, and evaluation targets (CedarBench + author-constructed external plans) are not independently audited production intent. That is a real scope limit, not a hidden inconsistency. The strongest claim—full 221/221 formal satisfaction of approved floors/ceilings/liveness, plus three corpus end-to-end verified stores—is supported by the stated CEGIS loop, signal-layer obligations (Table I, Alg. 2), ablations (Table III), property/request results (Tables V–VI), and Prop. 1's conditional soundness. No stronger load-bearing flaw (e.g., verifier–claim mismatch, unacknowledged circularity, or broken sandwich theorem) is required for the scoped claim to hold.","agreement_with_reader":"agree"},"referee_report":{"model":"grok-4.5","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.","tokens_in":17206,"tokens_out":1464,"duration_ms":17526,"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":[{"comment":"§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.","section":"§V.D RQ3; Table VI"},{"comment":"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.","section":"Abstract; §I Contributions; §V; §VI"},{"comment":"§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.","section":"§V.C Table III"}],"minor_comments":[{"comment":"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.","section":"§V.D Figures 3–4"},{"comment":"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.","section":"§III.A Algorithm 1"},{"comment":"§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.","section":"§V.A–B Table II"},{"comment":"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.","section":"§V.D.3"},{"comment":"Minor polish: consistent spacing around AUTOCEDAR (sometimes “AUTOCEDAR,” sometimes “AUTOCEDAR ”), and fix “OW ASP” → “OWASP” in the introduction.","section":"§I"},{"comment":"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.","section":"§VII"}],"recommendation":"minor_revision","confidential_remarks":"The paper is a good fit for a software-engineering / security venue that values systems + formal tooling. The conditional framing in Prop. 1 and §VI is more careful than the abstract; the main editorial risk is over-claiming “NL intent correctness” when evaluation targets are author-reviewed. I do not see a hidden circularity in the verifier loop itself once Π is fixed. Recommend minor revision rather than major: the three major points are scoping and evaluation-strength issues, not broken theorems or unreproducible core results. Code/benchmark release is a plus if the link remains live."},"author_rebuttal":null,"desk_editor":{"model":"grok-4.5","letter":"The thing worth knowing is that this is not another “LLM writes a policy” demo. They reverse the usual order: build a reviewed, checkable target first (schema + floors/ceilings/liveness), freeze it, then let the model propose under a CEGIS-style loop where the verifier owns accept/reject and a typed signal layer turns failures into TIGHTEN / LOOSEN / EXPAND without rewriting the target.\n\nWhat is actually new is the packaging. Intent atoms with dual mechanical/intent status, the synthesis sandwich (Theorem 1 is elementary but the right statement), and especially the signal-layer contract (Table I, Alg. 2) that keeps direction, witness, and history from collapsing into a vague “try again.” CedarBench (221 tasks with executable boundaries) and the three ACRE/REDE-derived end-to-end stores give them a real measurement surface. Empirically they deliver: 221/221 convergence, ablation residual loss from 15.58 down to 0 on the 100-scenario slice, and clear property/request wins over Category-2 direct generation. Prop. 1 is correctly conditional. Code is shipped.\n\nSoft spots, in proportion: organizational correctness is only as good as the human-approved plan. They say this plainly (Prop. 1, Threats). CedarBench plans and the external-corpus targets are author-constructed evaluation artifacts, not independently audited production intent. The human preference study is small and optional HITL feedback was sparse. None of that breaks the scoped claim; it bounds how far you can read the results.\n\nMath and citation pattern look fine—Zelkova lineage, CEGIS, LLM policy authoring, formal-feedback loops are placed honestly. No load-bearing circularity once Π is fixed; symcc is the oracle.\n\nThis is for people working on LLM-plus-verifier synthesis, authorization tooling, or security-sensitive code generation. It deserves a serious referee. I would engage with it, cite the architecture and CedarBench if I am in that space, and send it to peer review rather than desk-reject.","headline":"Solid systems paper: fixed-target authoring plus a typed repair signal for Cedar, with full-benchmark formal convergence and an honest conditional guarantee.","tokens_in":17866,"tokens_out":529,"would_cite":true,"duration_ms":8073,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":[],"pacs":[],"model":"grok-4.5","headline":"Access-control policies become trustworthy when reviewed intent is fixed first and a verifier steers the model until the policy matches that target.","keywords":["access control","Cedar policies","LLM synthesis","verifier-guided generation","policy authoring","CEGIS","intent atoms","authorization boundaries"],"falsifier":"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.","tokens_in":17817,"feed_emoji":"🔐","tokens_out":853,"duration_ms":17783,"temperature":0.7,"pith_summary":"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.","feed_headline":"Verifier loop turns access rules into proven Cedar policies","feed_subtitle":"Intent is fixed first; the model proposes until floors, ceilings, and live workflows all hold.","key_machinery":"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.","core_discovery":"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.","pith_inferences":["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."],"forward_implications":["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."],"fun_headline_variants":["Verifier loop synthesizes Cedar policies from reviewed intent","Fix intent first; AutoCedar steers models to verified Cedar rules","Intent atoms plus verifier feedback make policy authoring tractable","Reviewed targets hold while models repair until Cedar checks pass","Counterexample signals repair policies without altering approved intent"],"cache_read_input_tokens":128,"weakest_assumption_plain":"The guarantee only holds if the human-approved boundary plan truly captures what the organization meant to allow and deny.","fun_headline_variants_meta":{"raw":{"variants":["Verifier loop synthesizes Cedar policies from reviewed intent","Fix intent first; AutoCedar steers models to verified Cedar rules","Intent atoms plus verifier feedback make policy authoring tractable","Reviewed targets hold while models repair until Cedar checks pass","Counterexample signals repair policies without altering approved intent"]},"model":"grok-4.5","effort":"low","cost_usd":0.004286,"raw_usage":{"total_tokens":1335,"prompt_tokens":835,"num_sources_used":0,"completion_tokens":80,"cost_in_usd_ticks":42860000,"prompt_tokens_details":{"text_tokens":835,"audio_tokens":0,"image_tokens":0,"cached_tokens":256},"completion_tokens_details":{"audio_tokens":0,"reasoning_tokens":420,"accepted_prediction_tokens":0,"rejected_prediction_tokens":0}},"tokens_in":835,"tokens_out":80,"duration_ms":4012,"temperature":1.0,"reasoning_tokens":420,"cache_read_input_tokens":256,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-07-12T00:52:35.942068+00:00","model_set":{"reader":"grok-4.5"},"falsifier":"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.","supporting_citations":[],"review_version":1}