Automated Verification of Virtualized Infrastructures

Publication: Research - peer-reviewArticle in proceedings – Annual report year: 2011

View graph of relations

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
TitleCCSW '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
StatePublished

Conference

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

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

CitationsWeb of Science® Times Cited: No match on DOI

Keywords

  • Assurance, Formal specification, Virtualization, Cloud, Isolation, Information flow, System verification
Download as:
Download as PDF
Select render style:
APAAuthorCBEHarvardMLAStandardVancouverShortLong
PDF
Download as HTML
Select render style:
APAAuthorCBEHarvardMLAStandardVancouverShortLong
HTML
Download as Word
Select render style:
APAAuthorCBEHarvardMLAStandardVancouverShortLong
Word

Download statistics

No data available

ID: 6312616