School of
Electrical Engineering
and Computer Science

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


Research Leader

Post Docs and Seniors

Graduate Students

Project Members at SICS Swedish ICT

Former Project Members

  • Viktor Do (SICS)
  • Narges Khakpour (KTH)
  • Musard Balliu (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.


The project is funded by SSF.

Conference Publications

Cache Storage Channels: Alias-Driven Attacks and Verified Countermeasures
   Roberto Guanciale, Hamed Nemati, Christoph Baumann, and Mads Dam
   37th IEEE Symposium on Security and Privacy, 2016.

Automatic Derivation of Platform Noninterference Properties
   Oliver Schwarz and Mads Dam
   Software Engineering and Formal Methods (SEFM) 2016.

A high assurance virtualization platform for ARMv8
   Christoph Baumann, Mats Näslund, Christian Gehrmann, Oliver Schwarz, and Hans Thorsen
   European Conference on Networks and Communications (EuCNC) 2016.

Trustworthy Prevention of Code Injection in Linux on Embedded Devices
   Hind Chfouka, Hamed Nemati, Roberto Guanciale, Mads Dam, and Patrik Ekdahl
   European Symposium on Research in Computer Security (ESORICS), September 2015.

Trustworthy Memory Isolation of Linux on Embedded Devices
   Hamed Nemati, Mads Dam, Roberto Guanciale, Viktor Do and Arash Vahidi
   Trust and Trustworthy Computing (TRUST), August 2015.

Security Monitor Inlining and Certification for Multithreaded Java
   Mads Dam, Bart Jacobs, Andreas Lundblad, and Frank Piessens
   Journal of Mathematical Structures in Computer Science, Volume 25, Number 3, March 2015.

Trustworthy Virtualization of the ARMv7 Memory Subsystem
   Hamed Nemati, Roberto Guanciale, and Mads Dam
   SOFSEM 2015: Theory and Practice of Computer Science, January 2015.

Formal Verification of Secure User Mode Device Execution with DMA
   Oliver Schwarz and Mads Dam
   Hardware and Software: Verification and Testing. Haifa Verification Conference (HVC) 2014.

Automating Information Flow Analysis of Low Level Code
   Musard Balliu, Mads Dam and Roberto Guanciale
   Proceedings of the 21st ACM Conference on Computer and Communication Security (CCS'14) , Scottsdale, Arizona, USA, November 2014.

The Monotonic Separation Kernel
   Arash Vahidi
   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.


Formal verification of systems software: No execution of malicious software in Linux in networked embedded systems
   Jonas Haglund
   M.Sc. thesis. KTH, 2016.

No Hypervisor Is an Island: System-wide Isolation Guarantees for Low Level Code
   Oliver Schwarz
   PhD thesis, KTH, Trita-CSC-A 2016:22 (ISSN 1653-5723).

Logics for Information Flow Security: From Specification to Verification
   Musard Balliu
   PhD thesis. KTH, Trita-CSC-A 2014:13 (ISSN 1653-5723).

Inlined Reference Monitors: Certification, Concurrency and Tree Based Monitoring
   Andreas Lundblad
   PhD thesis. KTH, Trita-CSC-A 2013:01 (ISSN 1653-5723).

The Prosper run-time monitor: design and formal verification
   Hind Chfouka
   M.Sc. thesis, Pisa University, 2014.

A thin MIPS hypervisor for embedded systems
   Mikael Sahlström
   M.Sc. thesis, Lund University, 2013.

Porting Linux to a Hypervisor Based Embedded System
   Hariprasad Govindharajan
   M.Sc. thesis, Uppsala University, 2013.

Timevirtualisering för hypervisors
   Jonas Haglund
   B.Sc. thesis. KTH, 2012.


Main Project Page

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

Published by: Oliver Schwarz <>
Updated 2016-09-15