PROSPER: Provably Secure Execution Platforms for Embedded Systems

PROSPER is a collaboration between SICS and the Theoretical Computer Science group at KTH aiming 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. Our hypervisor is available as open source.
  • 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.

 Our industrial partners is Ericsson Research. The project is funded by SSF.

Publications
Number of items: 7.

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

Vahidi, Arash (2014) The monotonic separation kernel. In: 12th IEEE International Conference on Embedded and Ubiquitous Computing, 26-28 Aug 2014, Milan, Italy.

Schwarz, Oliver and Gehrmann, Christian and Do, Viktor (2014) Affordable Separation on Embedded Platforms: Soft Reboot Enabled Virtualization on a Dual Mode System. In: Trust & Trustworthy Computing (TRUST) 2014, 30 Jun - 2 Jul 2014, Heraklion, Greece.

Khakpour, Narges and Schwarz, Oliver and Dam, Mads (2013) Machine Assisted Proof of ARMv7 Instruction Level Isolation Properties. In: Certified Programs and Proofs (CPP), 11-13 December 2013, Melbourne, VIC, Australia.

Dam, Mads and Guanciale, Roberto and Khakpour, Narges and Nemati, Hamed and Schwarz, Oliver (2013) Formal Verification of Information Flow Security for a Simple ARM-Based Separation Kernel. In: 2013 ACM SIGSAC conference on computer & communications security, Berlin, Germany.

Vahidi, Arash and Jämthagen, Christopher (2013) Secure RPC in embedded systems - Evaluation of some GlobalPlatform implementation alternatives. In: 8th Workshop on Embedded Systems Security.

Schwarz, Oliver and Gehrmann, Christian (2012) Securing DMA through Virtualization. In: COMPENG 2012, 11-13 June 2012, Aachen, Germany.

This list was generated on Tue Mar 28 18:18:03 2017 CEST.