The PROSPER project has resulted in a number of achievements and assets, some of which are presented here divided in the following groups:
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.
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 (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.
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.
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.
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 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.
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.
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 is a VINNOVA project including SICS, Ericsson, ABB and Sectra, focusing on platform security for critical infrastructures.
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 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.