A Virtualization Assurance Language for Isolation and Deployment

Cloud computing and virtualized infrastructures are often accompanied by complex configurations and topologies. Dynamic scaling, rapid virtual machine deployment, and open multi-tenant architectures create an environment, in which local misconfiguration can create subtle security risks for the entire infrastructure. This situation calls for automated deployment as well as analysis mechanisms, which in turn require a cloud assurance policy language to express security goals for such environments. Where possible, configuration changes should be statically checked against the policy prior to implementation on the infrastructure. We study security requirements of virtualized infrastructures and propose a practical tool-independent policy language for security assurance. Our policy proposal has a formal foundation, and still allows for efficient specification of a variety of security goals, such as isolation. In addition, we offer language provisions to compare a desired state against an actual state, discovered in the configuration, and thus allow for a differential analysis. The language is well-suited for automated deduction, be it by model checking or theorem proving.