Toward a Query-Driven Approach for Formal Verification of Cloud Security Configuration

Managing security configuration in cloud environments is increasingly challenging due to their dynamism, and traditional manual inspection and testing are inadequate to ensure correctness and prevent misconfiguration. To address these issues, this paper introduces a query-driven formal verification approach that enables administrators to validate cloud security configurations using a high-level, user-friendly query language. Correctness is ensured by modeling the cloud environment and verification queries as a Satisfiability Modulo Theories problem, automatically solved by a state-of-the-art solver. Moreover, the approach covers diverse security aspects and detects complex multi-level attacks by integrating multiple security domains.