Verification of firewall reconfiguration for virtual machines migrations in the cloud

While elasticity is valuable to the cloud, it may introduce security flaws due to misconfiguration after virtual machines migration. In this paper, we propose an automated approach to verify distributed firewalls reconfiguration after migration. To this end, we elaborate a language that captures distributed stateless and stateful firewalls with their underlying semantics. Integrated to Cloud Calculus, it allows specifying distributed firewalls topology. We also define semantic equivalence over stateful firewalls that forms the base for our verification approach. Furthermore, we define the property of network access control and state preservation using the concepts of soundness and completeness of firewall configurations. Additionally, we use constraint satisfaction problems to reason about our defined preservation property. Finally, we investigate the correctness and scalability of our approach.