Objectives of this WP:

To develop type systems that guarantee adherence to security-related properties for global computing. In this period the particular properties and policies of interest are secure information flow, resource consumption, and alias control. Feasibility and practicability of these type systems will be demonstrated through prototype implementations by one of the industrial participants.

Security requirements concerning confidentiality or integrity can be expressed by restrictions on the permitted information flow within a system. This provides an adequate way of specifying confidentiality requirements such as ``a program's public output does not (explicitly or implicitly) reveal information about the program's secret input.'' Security type systems can be used to analyze automatically that the information flow within a program satisfies given restrictions or, in other words, that the information flow in the program is secure.

Basing on the output of Task 1.1, we will face the challenge of adapting information flow type systems to the setting of global computing as well as to real low-level languages, which is crucial as most code is distributed in this form. Thereby, we will also pave the way for a wider use of security type systems in the industrial development of security critical systems. Concretely, we will develop a type-based analysis of information flow security at the level of Java byte code. The fundamental scientific difficulty in developing a suitable type-based information flow analysis for global computers is the adequate treatment of concurrency and distributedness, which are inherent characteristics of global computers, in a low-level language like Java byte code. This is the main research problem that we will address in this task. Our preliminary studies of security type systems for simple multi-threaded and distributed languages have indicated the feasibility of statically ensuring confidentiality in the presence of a timing-sensitive attacker. Our profound experiences with the development of security analysis techniques for concurrent and distributed programstogether with the rich body of work on language-based security will provide the basis for meeting this challenge. Beyond concurrency, we will also investigate other important features of the Java byte code language such as exceptions and objects. Here, the main research goals will be to improve the somewhat naive treatment of exceptions in current security type systems and to integrate safety type systems within security type systems for arriving at a more precise analysis.

In this task, RWTH and CTH are jointly responsible for developing an adequate treatment of concurrency in the security analysis. We will use the study of information security for a simple multi-threaded and distributed language as a starting point. While useful for illustrating ideas, this language is unrealistically inexpressive. Furthermore, the security type system studied for this language is rather restrictive. Hence, the objective is to both (i) enrich the language with low-level primitives corresponding to a substantial subset of Java byte code and (ii) develop weaker observational security characterizations together with permissive type systems that enforce them.

Developing an adequate treatment of distribution in the security analysis is the responsibility of IC. This will include the investigation of features like marshalling and unmarshalling with RMI, code and program mobility, and class downloading.

INRIA is responsible for investigating other features of the Java byte code language than concurrency and, in particular, for improving the treatment of exceptions. INRIA is responsible for contributing to the integration of the developed solutions towards a sound security type system that covers most of the Java byte code language, including concurrency, exceptions, and objects. This integrated type system will be further improved in a joint effort by INRIA, RWTH, CTH, and IC in the second phase of the project (i.e. after T0+18).

This task depends critically on the input from Task 1.1.

The output of this task is critical input for Task 2.2 on mechanisms for safe information release and Task 2.6 on a prototype implementation of the type systems developed.

The result of this task is a report describing the type system developed and the insights gained. An intermediate report will be delivered after 12 months, as part of Deliverable D2.1 and will serve as input for Task 2.2, Task 2.6, and Task 3.5.

Task~2.2 Mechanisms for Safe Information Release, led by CTH.

As this task will not start in the first 18 months, we do not give a detailed implementation plan for it.

Task~2.3 Types for Basic Resource Policies, led by LMU.

This task aims at developing a type system for adherence to one of the basic resource policies developed in Task~1.2. The main difficulty lies in achieving a sufficient generality as to cover applications of real importance and yet remain tractable from an algorithmic and implementation point of view. There is a substantial piece of expertise with type systems for memory usage within the consortium and, more generally, within Europe which will allow us to make relatively rapid progress.

This task will focus on the most promising resource policy both in terms of industrial demand and realizability. We anticipate that this policy will relate to the issue of bounding parameters to system calls. For example, we may want to guarantee that a function performing network connections will not be called more than a certain number of times per minute and furthermore only with IP addresses falling into a certain range. We believe that many other concrete problems are of a similar nature. For example, parameters of calls to hardware related functions will need to observe certain safe limits. Initial studies in this direction have already been undertaken within MRG --- using dependent types and linear constraint solving techniques inspired by Dependent~ML --- but these need further development to be carried out by LMU and LFCS.

We will also explore the related methodologies of static analyses and automata-based techniques. INRIA will investigate means of expressing resource control based on the use of behavioral structures (automata, temporal logics, etc.). INRIA will design static data and control flow analyses for the JVM that will provide abstract interpretations of applets against which resource properties can be verified.

UPM will develop static analysis techniques for computing upper and lower bounds on resource consumption. This information will be used in Task~2.4 in order to guarantee that mobile code will not exceed the resources available on a given device.

At T0+12 an intermediate report on type systems for basic resource control will be produced as part of Deliverable~D2.1. We expect that this report will describe a type system for the selected basic resource policy in detail including typing rules and proof of soundness. The report will also contain comprehensive examples demonstrating the applicability of the system.

Task~2.4 Advanced Resource Policies and Optimization, led by LFCS

As this task will not start in the first 18 months, we do not give a detailed implementation plan for it.

Task~2.5 Alias Control Types, led by IC

The aim of this task is the development of powerful but lightweight confinement type systems for the source and byte code language, tailored to logical reasoning. The types will restrict to what extent an object may access or modify another one, in how far an expression may be the alias of another expression, and in how far some execution might affect some object. Such type systems will be used to support modular verification of functional and security properties, whereby the behavior of a class will be provable independently of its context of use. By lightweight we mean that the types should be easy to write, or to infer; we want to avoid some of the complexity of current parametric ownership type systems, and hope to find new solutions to open problems, such as ownership transfer. We also want to enhance the power of the system by using techniques from linear types which were proven successful for lower level languages, e.g. byte code, and adapting them to higher-level object-oriented languages. \\[\smallskipamount]

We will build on our earlier work, in particular \ETH has experience with Universe types, which are already part of JML and can be used to support modular verification, while IC has experience with ownership types, and their use to support verification. LMU has experience with the use of linear types to describe aliases for lower level languages.

In the first 18 months all four partners will collaborate on the definition of a containment type system for full Java, and the full byte code, as well as the description of the verifier. We will tackle type inference after the 18 month milestone.

One challenge for this period are the consideration of multi-threading and exceptions, the existence of least common supertypes, necessary for byte code verification. Another challenge is the adaptation of linear type systems to object oriented languages, and amalgamation with current confinement type systems; we expect to either enhance the containment type system, or possibly map the containment types in the Java-like language onto linear types at byte code level. ETH and IC will concentrate on the first, while LMU will concentrate on the latter challenge.

The results of these activities will be used in Task 3.4 (modular verification) and the case studies (WP~5).

At T0+12 we will produce an intermediate report describing the type systems for alias control for the source and the byte code language, as part of Deliverable~D2.1.

Task~2.6 Type System Prototypes, led by TL

The objective of this task is to develop a prototype implementation of the type systems defined in the other tasks of the work package in order to be able to evaluate them in practice and to use them to verify properties of actual applications. The prototype developed in this task should be the base of industrial-strength products; practical issues in the implementation of the type systems developed in Mobius will therefore be explored in great details.

The development work will be based on a generic library developed by TL for the static analysis of Java programs, which supports all the language's features, as well as some of the most common application frameworks (for instance, the MIDP framework and many of its extensions). This generic library has been developed since 2000, and it is the base of several static analysis marketed by TL on both the smart card and the mobile phone markets.

The main challenge in this task is to be able to implement on top of this existing system the type systems developed in Mobius. This challenge will be met progressively during the Mobius project, as the results from the other tasks in the work package become available.

Between T0+9 and T0+18, no actual result will be available. However, the directions in which the work starts is already known. The first task will therefore be the adaptation of the library to the category of type systems used in the project. This work can start very early, because it does not rely directly on the results of the Mobius project.

The objective is to obtain a new version of the generic library by T0+18, and to be able at that time to start the first experiments based on the type systems studied in the Mobius project.