Skip to main content

Provably secure virtualization

Mads Dam ( Dept. of Theoretical Computer Science, KTH Royal Institute of Technology )

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.



Share this: