Seminar 2016-05-18

2016-05-18

Speaker: Mads Dam, Dept. of Theoretical Computer Science, KTH Royal Institute of Technology

Bio

Mads Dam is PhD from Univ. Edinburgh and professor in Teleinformatics at the School of Computer Science and Communication, KTH, where he heads the Dept. of Theoretical Computer Science. Dam has an extensive track record in program verification and, more recently, computer security with more than 80 publications, many single authored, and many in top tier venues. He has received numerous grants and awards, from organisations such as the Swedish Research Council, the Swedish Foundation for Strategic Research, EU, Microsoft Research, and Ericsson. He has made influential contributions in a number of areas including linear and temporal logic, information flow analysis, compositional verification, and security monitoring. Currently he leads a team researching security kernels and hypervisors fully verified at system level for the ARM processor family.

Abstract

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.

Slides