Project Summary

This project aims at providing innovative, efficient and expressive mechanisms for the secure implementation and execution of code, with an emphasis on problems posed by embedded systems.

Innovative mechanisms are required to develop techniques that will allow embedded applications to be statically ckecked against safety policies, to self-adapt considering the availability of resources, and to perform software upgrades without human intervention. Safety policies can give end users protection from a wide range of flaws in binary executables, including type errors, memory management errors, violations of resource bounds, access control, and information flow.

As an enabling technology for the static and decentralized enforcement of complex and configurable security policies based on verifiable evidence, Proof Carrying Code (PCC) has been successfully applied in various contexts but, until now, little attention has been paid to applying these mechanisms to embedded systems. This forms the basis of the present project.

The very specific and constrained nature of the targeted embedded systems makes challenging the design and deployment of a flexible and efficient security enforcement architecture, but also makes it an ideal application area. New schemes have to be studied, implemented and deployed in order to turn PCC for embedded systems into a reality.

The design of PCC architectures has strong roots in foundational areas of Computer Science. These range from Type Systems, Computational Logic, and Proof Theory, to Programming Languages, Compiler Design, and Program Analysis techniques. New models are emerging that need to be further explored and matured in order to be used in embedded systems.

In this context, the proposal brings together a significant team of researchers from 5 different groups, comprising mathematicians, theoretical computer scientists, and experts in Embedded Systems, with the purpose of setting up a lasting scientific network in the area of Program Verification, with applications to Embedded Systems. The network has already given its first steps with the institution of a yearly event (The first "Jornada de Ciências da Computação" took place in June 2006 at FCUP), and the approved funding of several PhD students, to start working shortly on themes directly related to this proposal.

The design of such safety mechanisms will potentially give rise to a new embedded software paradigm. Safety certificates allow for new execution schemes where, for instance, (a) a program can provide static evidence that it will not use unsafe operations or resources; and (b) two applications can safely coexist in a embedded system.

Our roadmap in the present project proposal starts precisely with a clear identification of safety and security requirements and architectures for Embedded Systems. This is a crucial task, which will identify the policies to be statically enforced in our target systems, and used throughout the whole project.

Once the requirements have been identified, the challenge is to tackle the formalisation of the corresponding security and safety properties using different conceptual tools and different notions of safety certificate; we consider these grouped in the following three classes:

  • Type-based security enforcement mechanisms; here the goal is to study the use of typing features (such as type-and-effect analysis) as safety evidence, and to apply Type Inhabitance results to improve the proof infrastructure of a PCC platform.
  • Language-based security enforcement mechanisms, with the goal of studying the effect of certain language features (such as linearity or other forms of computational restriction that ensure "safety by construction") and compilation schemes on the architecture of the PCC platform.
  • Logic-based security enforcement mechanisms; this is the more traditional approach to PCC, but our perspective is to resort to source-level PCC, to allow for the use of techniques based on huigher-order logic (supported by the COQ toolkit and related tools), abstract interpretation (where we will continue previous work on the JaKarTa verification platform), and temporal logic / automata.

The final stage of the project consists in setting up a complete, working PCC backend platform for the static security enforcement mechanisms, and to provide a working deployment in embedded systems. These two tasks form the core of the applied component of the project. The approach is concluded by a complete and convincing case study, to form the proof of concept for the ideas arising from this project.

As a conclusion, the need for innovative security enforcement mechanisms in embedded systems and emerging PCC architectures prefigures the advent of a new, rich and unexplored research area which, we believe, will bring very interesting results and potentially give rise to a new perspective about software development.

Goals

The overall objectives of this project are the following, concerning code running in heterogeneous, potentially resource-limited embedded devices.

  1. The design of mathematically sound mechanisms for the static, formal assurance of safe and reliable execution.
  2. The design and implementation of a complete infrastructure for safe and reliable execution, based on Proof-carrying Code.
  3. To study and implement different scenarios for the deployment of safety mechanisms, specifically in embedded systems.

With such mechanisms, code that does not respect previously defined policies will be rejected and never installed or executed in a target device. This will allow to increase isolation guarantees and mobile code verification, which is of paramount importance in embedded systems.