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:
- A provably secure execution platform for embedded devices such as mobile phones based on a virtualization core
- A set of security services for monitoring, security policy enforcement and information flow control built on top of this platform
- A prototype toolset for formal specification and verification of the hypervisor, adaptable to different hardware architectures and hypervisor design choices, integrated into an Eclipse-based embedded systems IDE.
- 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
To appear at Certified Programs and Proofs (CPP) 2013.
Machine Code Verification of a Tiny ARM Hypervisor
Mads Dam, Roberto Guanciale and Hamed Nemati
To appear at TrustED 2013.
Formal Verification of Information Flow Security for a Simple ARM-Based Separation Kernel
Mads Dam, Roberto Guanciale, Narges Khakpour, Hamed Nemati and Oliver Schwarz
To appear in the Proceedings of the 2013 ACM SIGSAC Conference on Computer & Communications Security (CCS'13)
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)
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: November 01 2013.