Relia: Accelerating the Analysis of Cloud Access Control Policies
Abstract
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×.
BibTeX
@inproceedings{Wang-al:ASE25,
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},
title = {Relia: Accelerating the Analysis of Cloud Access Control Policies},
booktitle = {ASE},
pages = {228--240},
publisher = {{IEEE}},
year = {2025},
}