PROSPER

PROSPER achievements

The PROSPER project has resulted in a number of achievements and assets, some of which are presented here divided in the following groups:

Publications in conferences
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.
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.
Formal Verification of Secure User Mode Device Execution with DMA
Oliver Schwarz and Mads Dam
Hardware and Software: Verification and Testing, Springer LNCS 8855, proceedings of the Haifa Verification Conference (HVC), 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, and 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
Theses
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.
Test-benches and demonstrators
To demonstrate practical uses of the hyperviosr, we have configured a number of hardware and software test-benches, some of which are shown below
BeagleBoard-XM
The BeagleBoard-XM is a low-cost ARM development and prototyping board. The PROSPER project has used this board to demonstrate virtualization of embedded linux and provides source code, binaries and instructions for supporting this board.
BeagleBone
The BeagleBone is another low-cost ARM development and prototyping board similar to BeagleBoard-XM. It differs from the latter by being suitable for use in production due to its minimal design and extreme low cost. The PROSPER project is current using this board to test various network virtualization strategies under Linux.
NovaThor
The NovaThor is a mobile platform from ST-Ericsson. In past the NovaThor platform has been used by the PROSPER project to investigate combinations of hypervisor and TrustZone security.
Imperas OVP
The Imperas Open Virtual Platform (OVP) is a virtual modeling technology for simulating embedded systems with extreme details. The PROSPER project provides source code, binaries and instruction for executing the hypervisor on top of a simulated ARM Integerator platform which is the de facto industry standard for prototyping ARM system-on-chip or platforms.
QEMU
QEMU is a generic and open source machine emulator capable of running full-scale operating systems such as Linux with acceptable performance. The PROSPER project provides source code, binaries and instruction for executing Linux and the hypervisor on top of a emulated model of the BeagleBoard-XM, allowing everyone without access to development hardware and OVP licenses to test the hypervisor software.
Software
SICS Thin Hypervisor

The SICS thin hypervisor (STH) is a small hypervisor for embedded systems running on ARM. The open source version of the STH is capable of executing Linux on a number of popular development platforms.

STH is available under a number of open source licenses.

Monotonic separation kernel

The monotonic separation kernel is a special type of OS for resource constrained embedded system that provides a mechanism for logica separation of software components on hardware that do not support virtualization.

The hardware architecture supported by the monotonic separation kernel differs greatly from that of the STH. The kernel is therefore used to demonstrate the flexibility of the verification tools developed in the PROSPER project.

ENCoVer Tool

ENCoVer (Epistemic Noninterference COncolic VERifier) is a tool based on Java PathFinder and Z3, which we have developed for epistemic noninterference concolic verification. It addresses the problem of program verification for information flow policies by means of symbolic execution and model checking. Noninterference-like security policies are formalized using epistemic logic. Many scenarios considered tricky in the literature can be solved precisely using ENCoVer's approach. The provided link points to a page containg a detailed description, the bibliography and a reference to the binaries, along with installion instructions.

TreeDroid

An essential defensive security monitoring task is to determine and trace the flow of data through applications, OSs, and backend systems. TreeDroid is a security policy specification and enforcement framework for Android. It is based on tree automata and exploits taint tracking, a well known program monitoring technique. The results include fundamentals as well as tool support, implemented on top of the TaintDroid taint propagation tool for Android, originally developed at Penn State.

Models and Proofs
Isolation Properties on the ARM user mode ISA

When verifying security properties of a hypervisor, it is importnat to include the underlying hardware into the reasoning. In particular, in order to establish the isolation/bisimulation proofs we are after, it is necessary to make statements about how the system might change when the hypervisor has passed control to guests. Most projects simply assume isolation in user mode. PROSPER goes a step further and actually verifies what parts of the system user mode code can manipulate and/or read. This work builds upon the Cambridge HOL4 model of ARM. By now, our proofs have become part of the current official HOL4 release. The link above points to the corresponding GIT repository.

Collaborations and spin-offs
We have direct collaboration with about 20 industrial and academic partners. Below we list a selection of PROSPER's spin-off projects.
UaESMC

Usable and Efficient Secure Multiparty Computation (UaESMC) is a FP7 funded project between KTH, AS Cybernetica, the Univesity of Athens and the University of Tartu. The aim is to bring Secure Multiparty Computation (SMC) to a level where they can be applied to decisional and computational problems of practical size in several different social and economic sectors. SMC is potentially a fertile and novel application domain for embedded virtualization since it a) allows to solve problems involving multiple, mutually distrustful parties in a privacy preserving manners, and since b) the use of virtualization allows considerable savings in overhead due to the need to otherwise use physically separated platforms.

nSHIELD

nSHIELD is an EU FP7 ARTEMIS project working with measureable security for embedded devices. SICS has brought the knowledge on secure isolation by the usage of hypervisors on ARM into the project. Furthermore, some of the most resource intensive software development and platform adaptation work for the hypervisor used by PROSPER has been performed within nSHIELD.

As part of the collaboration within nSHIELD, the hypervisor has been analyzed in a security evaluation by SEARCH-LAB and has been enabled of launching through a secure boot by T2Data.

EMC2

Embedded systems enhance mechatronic products with cheaper and new functionalities and, as inter-system communication enabler, strongly support today's information society. The EMC2 project aims to develop an innovative, sustainable service-oriented architecture for mixed criticality applications in dynamic and changeable real-time environments, helping the European Embedded Systems industry to maintain its leading edge position.

EMC2 is an ARTEMIS-project, lead by Infineon. SICS as Swedish partner is focusing on the development of secure separation kernels for multicore systems.

MEDPRO

MEDRPRO is a VINNOVA project led by SICS and includes Sony Mobile Communications as partner. The focus lies on the usage of virtualization technologies for media data protection in mobile phones.

PSCIP

PSCIP is a VINNOVA project including SICS, Ericsson, ABB and Sectra, focusing on platform security for critical infrastructures.

MONITOR

MONITOR is an industry collaboration project between Ericsson and KTH in the auspices of the KTH ACCESS Linnaeus excellence centre. The goal of this short-term study is to use PROSPER project results on hypervisor verification and security monitoring to develop an application monitoring prototype for Ericsson.

HASPOC

HASPOC is a Vinnova sponsored project in Vinnova's Challenge Driven Innovation program. It is a second phase project and was defined in the first phase project Platform Security for Critical Infrastructures. The ultimate project target is to provide security for critical digital services and infrastructures by development of a trusted, cost and resource efficient virtualized COTS (ARMv8) platform with proven and Common Criteria certified security properties.