EnglishDTU.dkIndeksKontaktTelefonbogPortalenAlumnenetværk
Titel: Automated Verification of Virtualized Infrastructures
Type: Article in proceedingsArticle in proceedings
Person(er):
Forfatter:  Bleikertz, Sören
IBM Research, Zurich

Forfatter:  Gross, Thomas
University of Newcastle upon Tyne

Forfatter:  Mödersheim, Sebastian Alexander (Cwisno: 59879)
Technical University of Denmark
Email:

Uddrag: Virtualized infrastructures and clouds present new challenges for security analysis and formal verification: they are complex environments that continuously change their shape, and that give rise to non-trivial security goals such as isolation and failure resilience requirements. We present a platform that connects declarative and expressive description languages with state-of-the art verification methods. The languages integrate homogeneously descriptions of virtualized infrastructures, their transformations, their desired goals, and evaluation strategies. The different verification tools range from model checking to theorem proving; this allows us to exploit the complementary strengths of methods, and also to understand how to best represent the analysis problems in different contexts. We consider first the static case where the topology of the virtual infrastructure is fixed and demonstrate that our platform allows for the declarative specification of a large class of properties. Even though tools that are specialized to checking particular properties perform better than our generic approach, we show with a real-world case study that our approach is practically feasible. We finally consider also the dynamic case where the intruder can actively change the topology (by migrating machines). The combination of a complex topology and changes to it by an intruder is a problem that lies beyond the scope of previous analysis tools and to which we can give first positive verification results.
Publiceret: part of: CCSW '11 Proceedings of the 3rd ACM workshop on Cloud computing security workshop (ISBN: 978-1-4503-1004-8), pages: 47-58, 2011, ACM,
DOI:
Fil(er):
Præsenteret ved: ACM workshop on Cloud computing security workshop, Chicago, Illinois, USA
Se publikationen i DTU Orbit Se publikationen i DTU Orbit

Top
MatematiktorvetDTU - Bygning 303B2800 Kgs. LyngbyTlf. 4525 3031EAN-nr. 5798000428515
Cookies