Automated Verification of Virtualized Infrastructures

Sören Bleikertz, Thomas Gross, Sebastian Alexander Mödersheim

    Research output: Chapter in Book/Report/Conference proceedingArticle in proceedingsResearchpeer-review

    375 Downloads (Pure)

    Abstract

    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.
    Original languageEnglish
    Title of host publicationCCSW '11 Proceedings of the 3rd ACM workshop on Cloud computing security workshop
    PublisherACM
    Publication date2011
    Pages47-58
    ISBN (Print)978-1-4503-1004-8
    DOIs
    Publication statusPublished - 2011
    EventACM workshop on Cloud computing security workshop - Chicago, Illinois, USA
    Duration: 1 Jan 2011 → …
    Conference number: 3

    Conference

    ConferenceACM workshop on Cloud computing security workshop
    Number3
    CityChicago, Illinois, USA
    Period01/01/2011 → …

    Bibliographical note

    © ACM, 2011. This is the author's version of the work. It is posted here by permission of ACM for your personal use. Not for redistribution. The definitive version was published in CCSW'11, http://doi.acm.org/10.1145/2046660.2046672

    Keywords

    • Assurance
    • Formal specification
    • Virtualization
    • Cloud
    • Isolation
    • Information flow
    • System verification

    Fingerprint Dive into the research topics of 'Automated Verification of Virtualized Infrastructures'. Together they form a unique fingerprint.

    Cite this