Verifying conformance of security implementation with organizational access policies in community cloud a formal approach

In a community cloud, infrastructure is shared among several organizations from a specific community with common concerns (security, compliance, jurisdiction, etc.). In such a computing model, the security responsibilities rest mostly with the third-party infrastructure provider. Security violations may occur if local access policies from different organizations are not implemented correctly. Therefore, one of the major concerns for a cloud provider is to formally verify whether security implementation conforms to the local access policies, and ensure that shared resources (hosted in the multi-tenant infrastructure) are accessed by only authorized users from various organizations. In this paper, we propose an automated verification framework to address this issue of policy verification. The framework consists of two models: policy and implementation. An algorithm has been developed to reduce the models into Boolean clauses, and is given as input to zchaff SAT solver for formal verification. Experimental results show the efficacy of proposed approach.