Cloud calculus: Security verification in elastic cloud computing platform

Cloud orchestration involves cloud resources scaling up and down, management, as well as manipulation to better respond user's requests and to facilitate operational objectives of the service providers. These promote the elastic nature of cloud platform but force upon significant challenges to cloud service providers. Particularly, security issues such as inconsistency may arise while dynamic changes such as virtual machine migration occur. In this paper, we propose a formal framework for the specification of virtual machines migration and security policies updates. This framework enables us to verify that the global security policy after the migration is consistently preserved with respect to the initial one. To this end, we define a new calculus, namely cloud calculus that can be used to specify the topology of a cloud computing system and firewall security rules. It also enables specifying the virtual machines migration along with their security policies. The semantics of our calculus is based on structural congruence and a reduction relation. In order to verify the global security policy within the new configuration, we define a testing equivalence over cloud terms. Finally, we provide an illustrative case study to demonstrate the applicability of our approach.