用神经符号方法精准解析云权限策略，提升可读性与验证可靠性。
Neurosymbolic Characterization for Reliable Access Control Policy Analysis
- 结合有限状态自动机与大模型简化，生成可读的策略行为描述。
- 在3个云平台共746条策略上，平均相似度达0.93，比SMT基线提升2.7倍。
- 用户测试显示审查准确率从39%提升至93%，适合安全管理员使用。
访问控制策略是云系统中关键的可靠性配置，但管理员常难以验证策略是否仅允许其意图的行为。我们发现，无论使用推理型或非推理型大模型来生成策略，都无法以可靠精度理解策略语义，即使规范是模型自身解释也如此。这构成了「可验证合成悖论」：无论策略如何生成，验证鸿沟依然存在。为此，我们提出 PolicySummarizer，一种神经符号工具，通过有限状态自动机与基于大模型的简化，生成精确且人类可读的策略允许请求的刻画。该工具利用模型计数技术，确保生成结果的保真性，当相似度低于用户设定阈值时，自动采用形式化推导结果。在546条AWS、100条Microsoft Azure和100条Google Cloud Platform策略上，PolicySummarizer实现平均相似度0.93，较SMT基线提升2.7倍。用户研究表明，其将最难子任务的策略变更审查准确率从39%提升至93%，同时降低主观认知负担。我们已开源该工具。
原文摘要 · Abstract (English)
Access control policies are reliability-critical configuration artifacts in cloud systems, yet administrators frequently struggle to verify that a policy permits exactly what they intend. This verification gap cannot be remedied by using LLMs to synthesize policies: we find that reasoning and non-reasoning LLMs fluently explain policy behavior but cannot reason about policy semantics with reliability-grade precision, even when the specification is the LLM's own explanation. We formulate this impasse as the Verifiable Synthesis Paradox: the verification gap persists regardless of how the policy was authored. To remedy this, we introduce PolicySummarizer, a neurosymbolic tool that pairs finite-state automata with an LLM-based simplification to generate precise human-readable characterizations of requests allowed by a policy. PolicySummarizer uses model counting to guarantee the fidelity of the generated characterization by rejecting characterizations that fall below a user-configured threshold in favor of the formally derived one. On 546 AWS, 100 Microsoft Azure, and 100 Google Cloud Platform policies, PolicySummarizer achieves a mean similarity score of 0.93 and a 2.7x improvement over an SMT-based baseline. In a user study, PolicySummarizer raised policy-change-review accuracy from 39% to 93% on the hardest sub-task while reducing self-reported mental demand. We release PolicySummarizer as an open-source tool.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。