PROSPER (Provably Secure Execution Platforms for Embedded Systems) aims to build the next generation framework for fully verified, secure hypervisors for embedded systems. The following components constitute the core of the project:
The project is founded by the Swedish Foundation for Strategic Research (Stiftelsen för Strategisk Forskning - SSF).
- 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 the context of an ARM architecture.
News, Events, Media
- The open source version of the PROSPER "STH" hypervisor.
- Our work on the ISA isolation lemmas for user mode execution is available from the HOL4 GitHub site. Additionally, we keep some comments and a denser presentation on/of the assets on our homepage, as well.
Institutes and People
PROSPER is a cooperation between the Group for Theoretical Computer Science at the KTH Royal Institute of Technology (Stockholm, Sweden) and the Security Lab at SICS Swedish ICT (Kista, Sweden). The following people are involved:
Machine Assisted Proof of ARMv7 Instruction Level Isolation Properties
Narges Khakpour, Oliver Schwarz and Mads Dam
Certified Programs and Proofs (CPP) 2013.
Machine Code Verification of a Tiny ARM Hypervisor
Mads Dam, Roberto Guanciale and Hamed Nemati
Formal Verification of Information Flow Security for a Simple ARM-Based Separation Kernel
Mads Dam, Roberto Guanciale, Narges Khakpour, Hamed Nemati and Oliver Schwarz
Proceedings of the 2013 ACM SIGSAC Conference on Computer & Communications Security (CCS'13).
A Logic for Information Flow Analysis of Distributed Programs
18th Nordic Conference on Secure IT Systems, NordSec 2013, Ilulissat, Greenland, October 18-21, 2013.
(also available as extended version)
Secure RPC in Embedded Systems - Evaluation of some Global Platform Implementation Alternatives
Arash Vahidi and Christopher Jämthagen
8th Workshop on Embedded Systems Security (WESS 2013).
TreeDroid: A Tree Automaton Based Approach to Enforcing Data Processing Policies
Mads Dam, Gurvan Le Guernic, Andreas Lundblad
Proceedings of the 2012 ACM SIGSAC Conference on Computer & Communications Security (CCS'12).
ENCOVER: Symbolic Exploration for Information Flow Security
Musard Balliu, Mads Dam and Gurvan Le Guernic
Proceedings of the IEEE Computer Security Foundations Symposium (CSF '12 ). Harvard University, Cambridge MA, June 25-27, 2012.
Securing DMA through Virtualization
Oliver Schwarz and Christian Gehrmann
2012 IEEE Workshop on Complexity in Engineering (COMPENG 2012), 11-13 June 2012, Aachen, Germany.
Last modified: March 07 2014.