arXiv:2607.03656cs.SEcs.AI2026-07被引 1

用验证器引导生成安全的访问控制策略,避免代码通过但权限失控。

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

论文配图:AutoCedar: An Agentic Framework for Verifier-Guided Access Control Policy Synthesis
图 1 · 摘自论文原文
  • 将自然语言需求拆解为可审查的意图原子,分步验证
  • 在221个任务上全部收敛,生成可执行的正式策略
  • 适合需要高安全性的医疗、教育等场景的策略自动化

大型语言模型常被用于将自然语言需求转换为代码,但在访问控制中存在风险:生成的策略可能语法正确却授予未授权访问。问题不仅在于写代码,更在于明确需求含义并验证最终策略是否符合初衷。我们提出AutoCedar,一个验证器引导的框架:先将自然语言访问控制需求转化为可审查、可验证的目标,再基于该目标合成Cedar策略。AutoCedar将模式与策略编写分解为小规模的意图原子,包括词汇与行为的可审查声明。当这些原子通过机械验证和人工意图审查后,模型生成候选策略,验证器据此检查是否满足已批准目标;每次失败转化为修复信号,指导模型调整策略范围或结构而不改变目标。由于每一步都基于已审查意图并获得验证反馈,端到端策略生成变得可行。AutoCedar在我们构建的CedarBench基准(包含221个配对可执行语义边界的授权任务)上全部收敛。在涵盖医疗、教育和会议管理的三个需求语料案例研究中,AutoCedar成功将模糊的文本和提取的访问控制片段转化为经审查的模式、形式化检查及全局验证的Cedar策略库。

原文摘要 · Abstract (English)

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.

访问控制LLM生成策略验证

Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品;中文卡片由大模型生成,请以原文为准。