Provably secure virtualization

Virtualization is a promising technology to provide strong security guarantees in the presence complex and potentially compromised operating systems and application software. Within the Prosper project at KTH we have for a few years experimented with provable security for ARM-based virtualization solutions, primarily targeting mobile devices. This involves a number of topics: Processor modeling, verification tool development, hypervisor design for security, and the development of suitable verification techniques. In the talk I give an overview of progress made in the Prosper project in these areas, and discuss some of the directions our work is currently taking.