Provably secure virtualization
Mads Dam ( Dept. of Theoretical Computer Science, KTH Royal Institute of Technology )
- 11:00 30th October 2015 ( Michaelmas Term 2015 )Room 441
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.