Abstract

While elasticity represents a valuable asset in cloud computing environments, it may bring critical security issues. In the cloud, virtual machines (VMs) are dynamically and frequently migrated across data centers from one host to another. This frequent modification in the topology requires
constant reconfiguration of security mechanisms particularly as we consider, in terms of firewalls, intrusion detection/prevention as well as IPsec policies. However, managing manually complex security rules is time-consuming and error-prone. Furthermore, scale and complexity of data centers are continually increasing, which makes it difficult to rely on the cloud provider administrators to update and validate the security mechanisms.
In this thesis, we propose a security verification framework with a particular interest in the abovementioned security mechanisms to address the issue of security policy preservation in a highly dynamic context of cloud computing. This framework enables us to verify that the global security policy after the migration is consistently preserved with respect to the initial one. Thus, we propose a systematic procedure to verify security compliance of firewall policies, intrusion detection/prevention, and IPsec configurations after VM migration. First, we develop a process algebra called cloud calculus, which allows specifying network topology and security configurations. It
also enables specifying the virtual machines migration along with their security policies.
Then, the distributed firewall configurations in the involved data centers are defined according to the network topology expressed using cloud calculus. We show how our verification problem can be reduced to a constraint satisfaction problem that once solved allows reasoning about firewall traffic filtering preservation. Similarly, we present our approach to the verification of intrusion
detection monitoring preservation as well as IPsec traffic protection preservation using constraint satisfaction problem. We derive a set of constraints that compare security configurations before and after migration.
The obtained constraints are formulated as constraint satisfaction problems and then submitted to a SAT solver, namely Sugar, in order to verify security preservation properties and to pinpoint the configuration errors, if any, before the actual migration of the security context and the
virtual machine. In addition, we present case studies for the given security mechanisms in order to show the applicability and usefulness of our framework, and demonstrate the scalability of our approach.