一句话：将云访问控制策略翻译为 SMT 公式，借助模型计数求解器量化并比较策略的宽松程度。
云环境中的访问控制策略往往非常复杂，策略作者难以判断策略是否允许了非预期的数据访问。为此，作者提出 Quacky：给定一个策略，它将其翻译为 SMT 公式，并调用模型计数约束求解器来量化策略的宽松度（permissiveness）。当给定多个策略时，Quacky 不仅能判断哪个策略更宽松，还能量化策略之间的相对宽松度。该工具支持以 AWS IAM、Microsoft Azure 和 Google Cloud Platform（GCP）策略语言编写的访问控制策略，并提供命令行与 Web 两种界面。Quacky 是开源的，已在 GitHub 上发布，可帮助策略作者自动分析复杂策略，避免非预期访问。
quacky is a tool for quantifying permissiveness of access control policies in the cloud. Given a policy, quacky translates it into a SMT formula and uses a model counting constraint solver to quantify permissiveness. When given multiple policies, quacky not only determines which policy is more permissive, but also quantifies the relative permissiveness between the policies. With quacky, policy authors can automatically analyze complex policies, helping them ensure that there is no unintended access to private data. quacky supports access control policies written in the Amazon Web Services (AWS) Identity and Access Management (IAM), Microsoft Azure, and Google Cloud Platform (GCP) policy languages. It has command-line and web interfaces. It is open-source and available at https://github.com/vlab-cs-ucsb/quacky.
@inproceedings{paperbot7238,
title = {Quacky: Quantitative Access Control Permissiveness Analyzer✱},
author = {William Eiers and Ganesh Sankaran and Albert Li and Emily O'Mahony and Benjamin Prince and Tevfik Bultan},
booktitle = {ASE},
year = {2022},
doi = {10.1145/3551349.3559530}
}