Technical Summary: CloudFix

Problem Statement

Access control policies are critical for securing modern cloud computing environments, yet they are notoriously difficult to write and maintain. Administrators typically author these policies manually (e.g., using AWS IAM), a process that is tedious, error-prone, and requires significant domain expertise. Errors often lead to security vulnerabilities, such as overly broad permissions or unintended denials. While existing approaches using symbolic analysis have shown success in automated debugging, their generalizability to complex, cloud-based access control policies is limited. Conversely, Large Language Models (LLMs) have demonstrated success in automated program repair for general code, but their application to repairing access control policies remains unexplored.

Methodology: CloudFix

The authors introduce CloudFix, the first automated framework that integrates Large Language Models (LLMs) with formal methods to repair cloud access control policies. The system operates on an input policy and a specification of allowed and denied access requests. The repair process is iterative and consists of four distinct stages:

1. Goal Validation: The framework first evaluates the current policy against the request specification using an SMT solver (via the Quacky tool). If all requests are correctly classified, the process terminates. If misclassifications exist, the process proceeds to fault localization.
2. Fault Localization: This component identifies specific statements within the policy responsible for misclassifications. It categorizes faults into three types:
   • Case 1: Explicitly allowed statements that should be denied.
   • Case 2: Explicitly denied statements that should be allowed.
   • Case 3: Requests that are implicitly denied (due to lack of an allow statement) but should be allowed.
     The localizer uses an SMT solver (Z3) to determine which specific statements cause these errors.
3. Prompt Generation: The system constructs a prompt for the LLM. The authors compare two prompt strategies:
   • Baseline: Provides the faulty policy and the request specifications.
   • Fault Localization Guided: Augments the baseline with a structured report mapping specific failures to their root cause statements (e.g., "Statement V2 explicitly allows a request that should be denied").
4. Repair Synthesis: The LLM generates a candidate repaired policy based on the prompt. This candidate is returned to the Goal Validator. If it passes, the repair is complete; otherwise, the candidate becomes the input for the next iteration. The process continues until a fully repaired policy is found or a maximum iteration threshold is reached.

Key Contributions

The paper makes four primary contributions:

• Automated Repair Framework: The implementation of CloudFix, which automates the policy repair process using an LLM-driven, Fault Localization guided approach.
• Novel Integration: The first integration of LLMs with SMT-based formal verification specifically for repairing access control policies.
• Empirical Validation: Experimental evidence demonstrating that Fault Localization techniques significantly enable LLMs to repair faulty policies compared to baseline approaches.
• Public Resources: The release of a curated dataset of 282 real-world AWS IAM policies (extracted from forum posts) and the source code for CloudFix.

Experimental Results

The authors evaluated CloudFix using a dataset of 282 AWS IAM policies and synthetically generated request sets of varying sizes (10, 20, 30, and 50 requests).

• Effectiveness of Fault Localization: The Fault Localization guided approach consistently outperformed the baseline. For a request size of 10, the guided approach achieved an 84.0% full repair rate compared to 48.2% for the baseline. This advantage persisted as request sizes increased, with the guided approach maintaining a 54.3% full repair rate at 30 requests, while the baseline dropped to 22.3%. Statistical analysis (t-test) confirmed these improvements were significant (p < 0.001) for request sizes up to 30.
• Impact of Request Size: Repair accuracy generally degraded as the number of requests increased for both approaches. However, the guided approach degraded more gracefully. At 50 requests, the baseline achieved 0% full repairs, whereas the guided approach achieved 2.5% (7 policies).
• Model Performance: Among four open-source models tested (CodeLlama-7B, Llama-3.2-3B, DeepSeek-Coder-7B, Granite-3.3-8B), CodeLlama-7B-Instruct achieved the highest overall repair accuracy (92.3%) and the highest complete repair rate (54.3%).
• Generalization: Repaired policies demonstrated the ability to generalize to semantically similar requests not provided during the repair process. The Fault Localization approach achieved 84.9% accuracy on unseen variants, outperforming the baseline's 79.9%.
• Natural Language Synthesis: The framework successfully repaired policies when the request specifications were synthesized from natural language descriptions of user intent using an LLM (GPT-5), achieving 86.4% repair accuracy.
• Efficiency: The Fault Localization approach significantly reduced the number of iterations required for repair (e.g., 1.80 iterations vs. 3.14 for size 10), leading to faster total repair times despite the overhead of SMT solving.

Significance

The paper claims to be the first work to leverage LLMs specifically for the repair of access control policies. Its significance lies in demonstrating that combining the pattern recognition capabilities of LLMs with the rigorous correctness guarantees of formal methods (SMT solvers) creates a viable path for automated policy repair. The authors argue that this approach enables efficient, automated repair of cloud access control policies, addressing a critical gap where existing symbolic tools lack generalizability and pure LLM approaches lack formal verification. The work also highlights the potential for privacy-preserving repair using open-source models and the utility of fault localization in guiding LLMs through complex semantic reasoning tasks.