Policy synthesis method improves access control accuracy in natural language
RAISE: Reinforcing Access Control Policy Synthesis in LLMs via Symbolic Evaluation
Software EngineeringCryptography and SecurityMachine Learning
Summary
Creating computer policies that control who can do what is tricky when starting from everyday language. The authors made a big dataset called CedarInstruct that helps train and check these policies for correctness. They also designed RAISE, a training process that teaches language models to better understand and fix policy mistakes using formal checks. This approach helps the models write more accurate policies, outperforming other advanced language models.
What this means in practice
- •For security engineers: Automatically generate verified access control policies from natural language requirements to reduce manual coding errors.
- •For enterprise software developers: Enhance policy management tools by integrating formal verification guided learning to ensure precise authorization rules.
Authors
Yingming Zhou, Adarsh Vatsa, William Eiers
Abstract
Translating natural-language access-control requirements into policies requires careful reasoning about permissions, constraints, and exceptions, and even frontier LLMs often produce policies that violate the intended authorization semantics. We construct CedarInstruct, to our knowledge the first dataset that supports both training and semantic evaluation for formally verifiable Cedar policy synthesis. It contains 5,800 scenarios across 44 domains and 1,408 representing a single synthetic organization, each with a verified target policy and an executable verification plan. On this data we introduce RAISE, which trains policy synthesizers from formal verification in two stages, verified supervised fine-tuning (SFT) followed by a reinforcement learning (RL) stage that learns from verifier signal. We find that SFT succeeds largely by letting models express authorization logic they already have, since untrained models rarely write valid Cedar but often reason correctly when they do. After SFT, how the verifier's information is used matters more than how much of it is used. Of six RL instantiations that consume progressively richer verifier signal, only RAISE-OC improves meaningfully on SFT; it turns failed checks and symbolic counterexamples into guided exploration and learns from the result with off-context GRPO. With about 5.4K verified scenarios and LoRA fine-tuning, RAISE-OC trains Qwen3.5-9B to surpass zero-shot GPT-6 Astra and Claude Opus 5 by 13.33 and 16.26 percentage points in semantic success on held-out scenarios, and training transfers to the independently constructed CedarBench.