An Automated SMT-based Security Framework for Supporting Migrations in Cloud Composite Services

The growing maturity of orchestration languages is contributing to the elaboration of cloud composite services, whose resources may be deployed over different distributed infrastructures. These composite services are subject to changes over time, that are typically required to support cloud properties, such as scalability and rapid elasticity. In particular, the migration of their elementary resources may be triggered by performance constraints. However, changes induced by this migration may introduce vulnerabilities that may compromise the resources, or even the whole cloud service. In that context, we propose an automated SMT ¹ -based security framework for supporting the migration of resources in cloud composite services, and preventing the occurrence of new configuration vulnerabilities. We formalize the underlying security automation based on SMT solving, in order to assess the migrated resources and select adequate counter-measures, considering both endogenous and exogenous security mechanisms. We then evaluate its benefits and limits through large series of experiments based on a proof-of-concept prototype implemented over the CVC4 commonly-used open-source solver. These experiments show a minimal overhead with regular operating systems deployed in cloud environments.