Skip to main content
RISE logo

PROSPER: Provably Secure Execution Platforms for Embedded Systems

The PROSPER (Provably Secure Execution Platforms for Embedded Systems) project aims to build the next generation framework for fully verified, secure hypervisors for embedded systems.

The Provably Secure Execution Platforms for Embedded Systems (PROSPER) project aims to build the next generation framework for fully verified, secure hypervisors for embedded systems. It thus focuses on:

  • Isolation through Virtualization: One of our central assets is our hypervisor, a provably secure execution platform for embedded devices (such as mobile phones) based on a virtualization core. The hypervisor supports Linux as a guest and is available as open source.
  • Formal Verification: We developed a prototype toolset for formal specification and verification of different versions of the hypervisor, within the context of an ARM architecture.

Summary

Project name

PROSPER

Status

Completed

RISE role in project

Participant

Project start

Duration

5 Years

Partner

Royal institute of technology (KTH)