PROSPER

PROSPER project description

The following paragraphs aim at introducing the project in a nutshell:

Motivation

The use of software, including open source software, in the embedded domain is expanding dramatically and the volume of threats and attacks in the mobile domain is increasing. This comes in a situation where mobile communication has become the personal information platform of choice for a very wide range of the population, even in global terms. As a result, the particular value of the information carried by mobile devices, in terms of individual users financial, social, corporate assets, has increased, as new application platforms have gained acceptance that, for instance, may integrate PIN codes and access credentials in shared applications. But the aggregate value of that information, for instance in terms of preferences and behaviour has increased as well, useful for a variety of purposes, ranging from marketing and business intelligence to surveillance and political coercion. Especially the NSA revelations have shown to the general public how vulnerable all computing platforms, mobile ones included, are to subversion by a sufficiently powerful adversary. This also makes very apparent the case for openness and public verifiability in the realm of platform security, using devices like open source code, formal specification and verification, and publicly verifiable security certification, as suggested in the PROSPER project.

The long-term vision of PROSPER is the development of secure, formally verified and certified virtualization as the core building block, or root of trust, from which to bootstrap security in future embedded systems. The key property to be provided by such a platform is isolation: To allow different applications sharing the same hardware while preserving the confidentiality and integrity of their private data, both in terms of memory isolation (spatial isolation), and in terms of information flow and timing (temporal isolation), where this is necessary.

Foundations

The three foundations in the PROSPER project are Security, Virtualization and Formal Verification.

Security has started to become a major differentiator when it comes to the design of embedded systems. Security critical embedded devices are becoming pervasive and used for all manner of purposes, ranging from entertainment, media, and finance to embedded sensors and control systems in areas such as industry, power generation and transmission, transportation, and health.

As these embedded systems become increasingly networked, the opportunities for faults and abuse are multiplying, as are their potential to wreak havoc at both societal and individual level. The recent Stuxnet worm has significantly raised the bar on security countermeasures and amply demonstrates how vulnerable society is to attacks directed at its core infrastructure. This is likely to lead to a significantly increased demand for stronger security solutions in the embedded systems domain over the coming years.

Security concerns for embedded equipment range from reliability (high uptime, robust execution, network access etc.) to protection from software attacks such as viruses and trojans. In this project we address countermeasures against software attacks on embedded systems.

What we currently see is an explosion in the embedded software domain with respect to the number of applications and usage of open software. Open software platforms and operating systems also give more freedom and power to attackers, as source code documentation and common hacking tools are available. Hence, one would expect an increased threat to embedded systems in general. This is indeed happening, and a boost in mobile viruses and network attacks particularly targeting mobile devices or sensitive infrastructure embedded devices has been observed and recent attacks shows that infected application domains also can spread to core phone functionality, i.e., the baseband.

A hypervisor or Virtual Machine Monitor (VMM) runs at the most privileged execution level of the device and, with the help of the basic hardware protection mechanisms available on most platforms, is a powerful approach to provide both secure isolation and monitoring services. This is highly valuable as it allows trusted and untrusted applications to share the same hardware without interference.
Large open software systems subject to frequent updates are increasingly being expected to run on many embedded devices. In order to protect such a system, the key is a tamper resistant trusted computing base (TCB) that supports partitioning such that security-critical functions can be isolated from non-security-critical functions as well as providing the basis for a range of essential security services including monitoring, auditing, and access control. Today, there is a lack of hypervisors particularly designed to provide security for embedded systems. Consequently, Consequently, there is a unique opportunity for designs that can isolate critical security software components from open software components on embedded systems as well as provide software execution monitoring services. These new hypervisors should be able to run on a large set of different system on chip architectures.

In order to be attractive to the embedded software industry, formal proof of the hypervisor software security is most valuable as it can provide the kind of stringent evidence needed to make the new designs find their way to the market.

With a formal security proof developers are assured that - within an explicitly given set of assumptions - an implementation is guaranteed to behave as expected. In particular, as long as the assumptions are not violated, the implementation will be provably free of the 0-day attacks currently plaguing the IT industry .

So far, formal security proofs have been hard to utilize on a regular basis in the software development cycle. However, with the incremental improvements in verification technology over the recent years in areas such as theorem proving and automated software analysis, proving low-level software like a hypervisor or a security monitor correct has been transformed from a task which is virtually impossible to one which is still daunting, but nonetheless feasible. Our ambition is to expand tool support, theories, functionality, scope, coverage, and adaptability in both methodology and the range of hypervisors, processor architectures, and security issues that need to be addressed in an industrial context. We believe the combination of industrial pull for improved security analysis tools and the limited size and complexity of embedded systems software makes this an ideal case to push forward the industrial adoption of formal modelling and verification technology as a techniques for security and reliability also in a wider software engineering context

Concrete Goals and Objectives

The objective of the PROSPER project is to build the next generation framework for fully verified, secure hypervisors for embedded systems. The research program centres on the following three main problem domains:

  1. A provably secure execution platform based on a virtualization core.
  2. A set of security services for monitoring, security policy enforcement, and information flow control, built on top of this platform.
  3. A prototype toolset for formal specification and verification of the hypervisor, adaptable to different hardware architectures and hypervisor design choices.
The latter, in particular, involves both disciplinary progress on formalization, modelling, and verification tools and theories, as well as the systems research needed for hypervisor and services design, and demonstrator implementation.

Approach

One of the core assets of PROSPER is an in-house type-1 hypervisor, that is, a native hypervisor that is not running an any OS, but on bare metal. Its focus lies on providing security by MMU-supported separation. Following the system virtualization principle, it allows the parallel execution of multiple paravirtualized guests in user mode.

Both Linux and FreeRTOS have been ported to the hypervisor. Isolation between guests can intentionally be relaxed by the possibility to communicate with well-defined and parameterizable Remote Procedure Calls (RPCs) via the hypervisor. In addition to inter-guest-separation, the hypervisor offers introspection features such as virtual guest modes that enable intra-guest-separation as well, for example in order to maintain the guest OS' kernel separation even when executing in the processor's non-privileged operation mode. The implementation of the hypervisor comprises 2717 lines of C code and 942 lines of assembly, resulting in a compiled binary of 31 KB.

The hypervisor was developed for single-core ARMv5 and ARMv7 architectures and deployed on Beaglebone, Beagleboard, Beagleboard-xM, NovaThor and the Integrator development board, as well as on emulated platforms within the OVP framework or upon Qemu.

Different from other projects, in PROSPER we consider a setting where guests are supposed to be "isolated" while still having the possibility of communicating via RPCs. To verify our hypervisor we follow an approach where communication between partitions is made explicit in the top level specification (TLS), and information flow is analyzed in the presence of such an intended communication channel.

We formulate the TLS such that it directly formalizes, in sufficient detail, the set of computation paths both allowed and required at the implementation level, and then we check that the implementation indeed satisfies this specification. The question is how to do this, if it can be done while maintaining a satisfactory account of isolation, and if it can be done at a satisfactory level of abstraction (such that the TLS does not conflate to become identical to the implementation itself).

We aim to verify that there is no way for the partitions to affect each other, directly or indirectly, except through the intended channel. In particular, there should be no way for a partition to access the memory or register contents, by reading or writing, of the other partition, other than when the communication is realized by explicit usage of the intended channel, by both partitions in collaboration. This is not an easy property to reconcile with the standard information flow tools such as noninterference. After all, the very purpose of the kernel is to allow rather than prevent information flow (through the intended channel). We thus take a different approach. We formulate the TLS as an "ideal model" which satisfies the required separation properties by construction, and then reduce correctness to trace equivalence w.r.t. a "real model", reflecting actual systems behaviour. The key idea is to execute the partitions on physically separate, ideal processors, connected by an explicit, ideal communication channel, and equipped with a little extra paraphernalia. The ideal processors need to accurately mimick the execution of user space partitions on a real processor. This is done by augmenting the TLS processors by idealized functionality, which is invoked whenever the actual processors would transition to privileged mode by an exception (e.g. a hardware interrupt, or an exception). This construction allows userland code to execute as desired, but the idealized processors are physically prevented from directly affecting their sibling machine, with the exception of explicit communication using the message delivery service. The task is thus to show that, properly set up, the user observable traces of the ideal model are the same as those of a "real model", obtained by executing the software in different partitions on top of our separation kernel, on top of a real ARMv7-A processor, including a Memory Management Unit (MMU) for physical protection of memory regions belonging to different partitions. We prove this using the bisimulation proof method, by exhibiting a concrete bisimulation relation, a candidate relation, relating the state spaces of ideal and real models. The proof that the candidate relation is actually a bisimulation relation of the appropriate type is in turn reduced to subsidiary properties, several of which have natural correspondences in previous kernel verification literature, namely that:

  1. The initial states of the ideal and the real models are in the candidate relation. This is ensured by the correctness of the bootstrap code.
  2. A partition does not perform any isolation-violating operation while it is executing. Due to our use of memory protection, this is really a noninterference-like property of the ARMv7-A architecture rather than a property of the separation kernel.
  3. The processor state switches correctly upon transition to privileged mode. Again this is a processor architecture rather than a kernel dependent result.
  4. Execution of ideal exception handlers vs the real separation kernel exception handlers preserve the candidate relation.
  5. Several invariants are preserved while partitions and/or kernel handlers are running.
For the actual verification we have used a combination of theorem proving and binary code analysis. The real and ideal models are built on top of the Cambridge ARM HOL4 model, extended with a simple MMU unit. The isolation lemmas of ARM are proved using a tool, ARM-prover, developed for the purpose in HOL4. The proofs are costly and involve traversing the full ARM instruction sets. The ARM-prover allows the proofs to be automated to a large extent. This frees us from the task of verifying the two theorems on each element of the large ARM instruction set. Handlers are verified using pre/post conditions. Manual generation of these handlers is an error-prone process, and for this reason we generate the pre/post conditions automatically based on the specification of the ideal model, the candidate relation, and the ARM isolation Lemmas. We transfer the pre/post conditions to the binary code analysis tool BAP, and use BAP to verify the bootstrap code and the kernel handlers at the assembly code level. Several tools have been developed for lifting the ARM code to the input format of BAP and manipulating the code.

To get some more details, you are welcome to watch a one hour long presentation (457 MB) which Mads Dam gave in Rennes in February 2014:

Milestones

In the autumn of 2013 the project reached the first major milestone, the design and full formal specification and verification of version 0 of the PROSPER hypervisor.

The objective of this milestone was to bring together all branches of the project for the end-to-end specification, design, verification, implementation, and test, of a first proof-of-concept hypervisor, in order to establish a common view and technical platform for the entire project, and set the stage for later development. The functionality of the version 0 hypervisor was deliberately kept very slim, essentially restricting to context switching between a number of statically assigned guest systems, and a hypercall for explicit asynchronous communication between guest systems. This is barely enough to run, e.g., two control loops in parallel that pass messages between each other and interact with some simple (non-DMA) memory-mapped sensor or actuator. The verification, however, is very comprehensive, and offers several novel results, in that we cover information flow at a very detailed level, and give a top-level specification of the security property as a novel ideal model construction1. We are to our knowledge the first to establish such a comprehensive analysis for a commodity processor architecture (ARMv7), including hardware memory protection. The work is also first to perform this analysis at the system level, covering both handler-specific properties and properties dependent on the hardware platform, to account for statically unknown user-mode execution. Furthermore, the tool we developed for instruction level analysis represents to our knowledge the first comprehensive formal security analysis of the ARMv7 instruction level architecture. We note that the version 0 hypervisor has been implemented and ported to our emulation platform OVP, and slight variations of the kernel have been ported to Beagleboard, Beagleboard XM, NovaThor, and the Integrator development board.

The open source version of the hypervisor supports now both FreeRTOS and Linux as guest operating systems.

Linux virtualization requires memory management (MMU) support for kernel mode protection, and the support of multiple OS modes (user, kernel, other) as separate guest systems is not appropriate for delegation to an external, hypervisor level scheduler. For this reason we have developed a single guest, multiple mode hypervisor, STH, ported Linux kernel version 2.26 to it, and released this hypervisor in open source form. The STH hypervisor is currently undergoing redesign and verification, and it forms the basis for the PROSPER version 1 hypervisor.

The version 1 hypervisor will be a crucial milestone for PROSPER. It will be, to the best of our knowledge, the first time memory isolation will have been formally established for Linux and, indeed, for any application OS. This will be a highly significant result in its own right. In more technical terms it is also important to establish the ability and performance costs of running Linux on top of our hypervisor, and it is of high interest to develop the skills and understand the complexities involved in porting Linux to our paravirtualized hypervisor platform.

Further Activities

An essential defensive security monitoring task is to determine and trace the flow of data through applications, OSs, and backend systems. We examined the use of taint tracking, a well known program monitoring technique, for security policy enforcement on Android, and presented TreeDroid, a policy specification and enforcement framework based on tree automata. 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.

Several of our works have examined device virtualization, including direct memory access (DMA) and timer virtualization. Both types of device virtualization pose interesting challenges from both a systems and a verification point of view, as they can affect guest observable properties in interesting ways. Timing and device virtualization remains active items on the PROSPER research agenda.

Several of our works have explored information flow analysis from perspectives that have gradually become more directly relevant for PROSPER. We explore epistemic logic (logics of knowledge) as a natural tool for specifying practical information flow security properties. This has been developed further and applied to increasingly low-level languages. We showed how to algorithmically solve "bounded" information flow problems at Java bytecode level.

Partners and Advisory Boards

Ericsson is the main partner of PROSPER and a world-leading provider of telecommunications equipment and services to mobile and fixed network operators. Over 1,000 networks in more than 180 countries use our network equipment, and more than 40 percent of the world's mobile traffic passes through Ericsson networks.


ST-Ericsson was a joint-venture between Ericsson and STMicroelecetronics and until its split-up in 2013 our second project partner. It was a world leader in developing and delivering a complete portfolio of innovative mobile platforms and cutting-edge wireless semiconductor solutions across the broad spectrum of mobile technologies.


To the project is associated an industrial and a scientific advisory board. Members of the industrial advisory board (IAB) are the industrial collaborators, Dr Mats Näslund, Ericsson Research, and Dr Per Ståhl, Ericsson Modems, formerly with ST/Ericsson. The IAB has met three times during the first half of the project. Members of the scientific advisory board (SAB) are prof. Bart Preneel, KU Leuven, and prof. Gilles Barthe, IMDEA, Madrid. The SAB has met once during the first half of the project.