一句话：提出基于SMT与模型计数的定量符号分析，自动修复过度宽松的访问控制策略。
云访问控制策略复杂，管理员易无意授予过多权限，导致数据泄露。本文提出一种定量符号分析策略修复方法，针对过于宽松的访问控制策略。方法用SMT公式编码策略语义，并以模型计数衡量其宽松程度；给定策略、宽松度上界和一组必须允许的请求，迭代执行宽松度削减与精化，在仍允许指定请求的同时使策略满足宽松度上界。作者将技术应用于Amazon AWS IAM策略语言，展示自动修复的有效性。
With the growing prevalence of cloud computing, providing secure access to information stored in the cloud has become a critical problem. Due to the complexity of access control policies, administrators may inadvertently allow unintended access to private information, and this is a common source of data breaches in cloud based services. In this paper, we present a quantitative symbolic analysis approach for automated policy repair in order to fix overly permissive policies. We encode the semantics of the access control policies using SMT formulas and assess their permissiveness using model counting. Given a policy, a permissiveness bound, and a set of requests that should be allowed, we iteratively repair the policy through permissiveness reduction and refinement, so that the permissiveness bound is reached while the given set of requests are still allowed. We demonstrate the effectiveness of our automated policy repair technique by applying it to policies written in Amazon's AWS Identity and Access Management (IAM) policy language.