Publications
Astragalus: Automatic Configuration Repair for Production Networks
Research Area: Network Verification, Software Engineering
Abstract
Network configurations are prone to errors, which can lead to catastrophic service outages. A tool that can achieve automatic configuration repair (ACR) is highly desired by operators. Existing tools for ACR follow a semantic-driven approach: they model network semantics as a set of SMT constraints, and solve them for a location or fix of the error. Due to the complex semantics of networks, constructing and solving these constraints can be prohibitively expensive, making these tools neither general nor scalable. Inspired by automatic program repair (APR), we explore another direction, i.e., a syntax-driven approach, which tries to repair program bugs by “grafting” some existing code in the same repository, without modeling program semantics. Following this direction, we propose Astragalus, a syntax-driven method for ACR. It uses multiple iterations of a “localize-fix-validate” pipeline to search for repairs, and proves quite effective on configurations of our production network. Specifically, we show that Astragalus can repair every incident in multiple sizes of a synthesized network, and 97.5% of the incidents on a real network, both with 15 types of errors injected, within an average time of 7.36 seconds. It has also provided valid repair options in under 6 minutes for 4 recent network incidents or undesired changes, in a real production network with O(1,000) ~ O(10,000) devices.
BibTeX
@misc{gu2026astragalus,
title={Astragalus: Automatic Configuration Repair for Production Networks},
author={Zhenrong Gu and Peng Zhang and Xing Feng and Xu Liu},
year={2026},
eprint={2605.22092},
archivePrefix={arXiv},
primaryClass={cs.NI},
url={https://arxiv.org/abs/2605.22092},
}
Relia: Accelerating the Analysis of Cloud Access Control Policies
Research Area: Formal Methods, Software Engineering
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{wang2025relia,
title={Relia: Accelerating the Analysis of Cloud Access Control Policies},
author={Wang, Dan and Zhang, Peng and Gu, Zhenrong and Lin, Weibo and Jiang, Shibiao and He, Zhu and Du, Xu and Chen, Longfei and Li, Jun and Guan, Xiaohong},
booktitle={2025 40th IEEE/ACM International Conference on Automated Software Engineering (ASE)},
pages={228--240},
year={2025},
organization={IEEE}
}
AccessRefinery: Fast Mining Concise Access Control Intents on Public Cloud
Research Area: Formal Methods, Software Engineering
Abstract
Modern cloud applications heavily rely on Identity and Access Management (IAM) services to enforce flexible access control over their data. However, the flexibility comes at a cost: IAM policies are often complex and prone to misconfigurations, leading to risks of data exposure. There is an increasing need to mine a compact set of intents that describe what the policies collectively try to achieve, thereby enabling operators to better understand their policies. However, existing tools on mining access control intent have two major limitations: (1) the mining process is slow and even times out on some complex policies; (2) the mined intents are excessive in number and thus still hard to understand. To overcome these limitations, this paper presents AccessRefinery, which can speed up the mining process while reducing the number of intents. The key idea for the speedup is to reduce the redundancy of the multi-round SMT solving, by preprocessing the constraints into bit-vector constraints. For intent reduction, AccessRefinery computes a compact set of intents that can cover the mined intents, by solving a min-set-cover problem. Experiments based on real and synthetic datasets show that AccessRefinery achieves a ~10–100× speedup in intent mining, and reduces the number of intents by up to ~10×.