PROSPER: Provably Secure Execution Platforms for Embedded Systems

PROSPER is a collaboration between SICS and the Theoretical Computer Science group at KTH aiming to build the next generation framework for fully verified, secure hypervisors for embedded systems. The following components constitute the core of the project:

  • A provably secure execution platform for embedded devices such as mobile phones based on a virtualization core. Our hypervisor is available as open source.
  • A prototype toolset for formal specification and verification of different versions of the hypervisor. Within this work, ISA isolation lemmas for user mode execution on ARM have been verified. Those proofs are available from the HOL4 GitHub site.

 Our industrial partners is Ericsson Research. The project is funded by SSF.