Virtual machines are an integral part of public-cloud offerings. In this setting, customers rely on the provider to ensure a secure and reliable operating platform. Isolation from other – possibly malicious – guests is of utmost importance. The core components are hypervisors and device emulation on top of a Linux kernel. In this talk I will discuss the challenges in performing software analysis for such a stack, and how automated static analysis ranging from data-flow analysis to model checking helps to identify and resolve issues.