bild
School of
Computer Science
and Communication

^ Up to Research, Theory group at Nada, KTH.

PROSPER

Research Leader

Post Docs and Seniors

Graduate Students

Project Members at SICS Swedish ICT

Former Project Members

  • Viktor Do (SICS)
  • Narges Khakpour (KTH)

Short Description

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:
  1. A provably secure execution platform for embedded devices such as mobile phones based on a virtualization core. Our hypervisor is available as open source.
  2. 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.
PROSPER is a cooperation between the Group for Theoretical Computer Science at KTH and the SICS Swedish ICT.

Funding

The project is funded by SSF.

Related Publications

The Monotonic Separation Kernel
   Arash Vahidi
   To appear in the 12th IEEE International Conference on Embedded and Ubiquitous Computing, Milan, Italy, 26-28 August, 2014.

Affordable Separation on Embedded Platforms: Soft Reboot Enabled Virtualization on a Dual Mode System
   Oliver Schwarz, Christian Gehrmann and Viktor Do
   Proceedings of Trust and Trustworthy Computing (TRUST) 2014.

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
   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
   Proceedings of the 2013 ACM SIGSAC Conference on Computer & Communications Security (CCS'13).

A Logic for Information Flow Analysis of Distributed Programs
   Musard Balliu
   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.

Links

Main Project Page

^ Up to Research, Theory group at Nada, KTH.

Published by: Oliver Schwarz <oschwarz@kth.se>
Updated 2014-07-10