TY - GEN

T1 - Automated Verification of Virtualized Infrastructures

A1 - Bleikertz,Sören

A1 - Gross,Thomas

A1 - Mödersheim,Sebastian Alexander

AU - Bleikertz,Sören

AU - Gross,Thomas

AU - Mödersheim,Sebastian Alexander

PB - ACM

PY - 2011

Y1 - 2011

N2 - 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.

AB - 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.

KW - Assurance

KW - Formal specification

KW - Virtualization

KW - Cloud

KW - Isolation

KW - Information flow

KW - System verification

UR - http://crypto.cs.stonybrook.edu/ccsw11/

U2 - 10.1145/2046660.2046672

DO - 10.1145/2046660.2046672

SN - 978-1-4503-1004-8

BT - CCSW '11 Proceedings of the 3rd ACM workshop on Cloud computing security workshop

T2 - CCSW '11 Proceedings of the 3rd ACM workshop on Cloud computing security workshop

SP - 47

EP - 58

ER -