Cloud Security Verification

Cloud7 Overview of our architecture for tool-supported infrastructure cloud analysisWe pursue the verification of security properties of infrastructure clouds. See talks at EU CSP'12 or ACM CCSW'11.

We consider two domains:

  • Topology of the infrastructure, that is, how VMs, hosts, networks and storages are inter-connected, and
  • Dynamics of re-configuration, that is, how administrators can change the topology and privileges with cloud operations.
  • We compare the actual state of the configuration with a desired state specified in formal language.

Approach: Actual State vs. Desired State

  • Actual state: Tools discover the actual configuration of the virtualized infrastructure and derive a graph/term representation.
  • Desired state: Security goals are specified in a high-level language, which defines attack states as patterns of facts with logical constraints.

We apply model checking to verify that the topology is free of security violations (static case) or that administrators cannot reach a state that violates the policy by their cloud operations (dynamic case).

We analyzed isolation security for a production infrastructure of a global financial institution.

Open PhD Position

PhD in Security Verification of Dynamic Infrastructure Clouds (CS033)


The research prototype of our cloud security assurance analysis has been transferred to IBM as part of the IBM PowerSC Trusted Surveyor product in 2012. The research started during my time at IBM Research and continued in an industry collaboration at Newcastle.

Image Gallery

Selected Presentations

EU Cyber Security and Privacy Forum 2012

Verification of Infrastructure Clouds (ACM CCSW'11)

Selected Papers

Sören Bleikertz, Thomas Groß, and Sebastian Mödersheim. Automated Verification of Virtualized Infrastructures. In Proceedings of the CCS Cloud Security Workshop(CCSW) 2011.

Sören Bleikertz and Thomas Groß. A Virtualization Assurance Language for Isolation and Deployment. In proceedings of IEEE POLICY 2011.

Sören Bleikertz, Thomas Groß, Matthias Schunter, and Konrad Eriksson. Automated Information Flow Analysis of Virtualized Infrastructures. In Proceedings of the European Symposium on Research in Computer Security (ESORICS) 2011.