Analyzing Component Composability of Cloud Security Configurations

Security is a major concern when building large-scale computer systems. Cloud services have made it easier to provision large-scale systems on demand over the Internet. While the cloud service providers provide the required building blocks such as compute units, database servers, and storage, customers are still responsible for securely combining these systems to satisfy their organization's security policy. The secure development and operation of such large-scale systems present technical challenges. Composing a larger system using components with known security properties that satisfy a given security policy without re-analyzing the individual components is a difficult problem. In this study, we attempted to analyze the composability of components from a security perspective using first-order predicate logic. We posit that if we build a system using individual components that satisfy a security policy, the composed system will be sound with regard to that policy. Additionally, the methodology can be used to identify drifts or violations during future changes in the system by running checks during the system release cycles for continuous verification.