We consider two domains:
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.
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.
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.