一句话：提出 Relia，用字符串等价类将正则约束重写为整数约束，加速云访问控制策略的 SMT 分析。
云服务访问控制策略配置易错，云厂商用 SMT 工具形式化分析用户策略，但策略中复杂正则匹配条件导致分析缓慢。Relia 的核心是依据策略中的正则表达式预计算一组字符串等价类（SEC），为每个类分配唯一整数，并将正则约束重写为等价的整数约束，使 SMT 求解更高效；它作为内部访问分析器与现成 SMT 求解器之间的透明层实现。基于某大型公有云的真实策略评估，启用 Relia 后，由 Z3、Cvc4、Cvc5 组成的内部组合求解器对近 95% 的案例加速，平均加速 8.21 倍。
With the diversification of cloud services, cloud providers offer flexible access control by letting users apply fine-grained cloud access control policies to secure their cloud resources. However, flexibility comes with the cost that configuring cloud access control policies is error-prone. Therefore, cloud providers have developed SMT-based tools to formally analyze the user-defined policies. Unfortunately, we find these analyzers slow, due to the complex regular expression matching conditions in policies. To this end, this paper introduces Relia, a general method to speed up the analysis of cloud access control policies. The key idea of Relia is to pre-compute a set of String Equivalence Classes (SECs) based on the regular expressions in a policy, assign a unique integer to each SEC, and rewrite the regular constraints into equivalent integer constraints, which are easier to solve. We implement Relia as a transparent layer between our in-house access analyzer and off-the-shelf SMT solvers. Based on real policies from a large public cloud provider, we show that: when enabling Relia, our in-house portfolio solver (consisting of Z3, Cvc4, and Cvc5) can speed up the analysis process for nearly 95% of all cases, with an average speedup of 8.21×.
DOI 原文 ·
@inproceedings{paperbot9322,
title = {Relia: Accelerating the Analysis of Cloud Access Control Policies},
author = {Dan Wang and Peng Zhang and Zhenrong Gu and Weibo Lin and Shibiao Jiang and Zhu He and Xu Du and Longfei Chen and Jun Li and Xiaohong Guan},
booktitle = {ASE},
year = {2025},
doi = {10.1109/ase63991.2025.00027}
}