Write a Blog >>

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.

Thu 22 Jun

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

13:40 - 15:00
Academic C-verification project; industry perspective on hypervisorsDSW at Vertex WS216
Chair(s): Adam Chlipala Massachusetts Institute of Technology, USA
13:40
40m
Talk
Verifying concurrent C programs with the Verified Software Toolchain
DSW
Andrew W. Appel Princeton
14:20
40m
Talk
Challenges in Analysing Virtualisation Stacks
DSW
Michael Tautschnig Amazon Web Services