MOBIUS - Securing the Next Generation of Java-Based Global Computers

by Gilles Barthe

Global computers have the potential to realize the vision of ambient intelligence and to offer citizens a global and uniform access to services. Yet their success is conditioned by the development of appropriate security architectures that help establish trust and security in a global setting. Within the Global Computing 2 initiative, the FET Integrated Project 'MOBIUS' aims at providing the technology for securing next-generation global computers, building on the Proof Carrying Code paradigm.

Global computers aim at providing a global and uniform access to services through distributed computational infrastructures consisting of very large numbers of interacting devices. Prominent examples include the Internet, banking and telephone networks, digital video infrastructures, peer-to-peer and ad hoc networks.

While global computers may profoundly affect our quality of life, they will only become pervasive if novel security architectures are developed for bringing to users the level of reliability and security they expect for sensitive services. To realise this aim, the project will develop and combine type systems and program logics that can be used to ensure functionality and security policies for Java-enabled global computers.

Next Generation Global Computers
The next generation of global computers will emphasize the emergence of infrastructures with increasingly autonomous and heterogeneous devices:

autonomy: devices will not be subjected to a global and uniform control, may belong to several global computers and may even move between different global computers
heterogeneity: devices shall present significant differerences in their computational infrastructure (operating systems, communication protocols, libraries) and resources (memory, power autonomy, connectivity).

In order to accommodate these trends, the next generation of global computers will also require that devices are extensible with the computational infrastructure, platform or libraries needed to execute services as requested. This evolution will cause global computers to escape the scope of computational models which permeate mobile code, the Grid, or agents, and which impose a sharp separation between untrusted mobile applications, and the fixed and trusted computational infrastructure upon which they execute. At the same time, the evolution towards autonomy and extensibility will create new security threats that would not be found in current computational models, and thus any security architecture for global computing must comply with requirements that reach far beyond the limits of the current state-of the art.

A Security Architecture based on Verifiable Evidence
The objective of the Mobius project is to develop a security architecture that meets the needs of global computers, by providing:

innovative trust management, dispensing with centralized trust entities and allowing individual components to gain trust by providing verifiable evidence that they do not affect the security of the overall system
static enforcement mechanisms, sufficiently flexible to cover the wide range of security concerns arising in global computing, and sufficiently resource-aware and configurable to be applicable to the wide range of devices in global computers
support for system component downloading, for compatibility with the view of a global computer as an evolving network of extensible devices.

The security architecture builds on ideas from Proof Carrying Code (PCC), and requires that mobile code is provided with a certificate, ie a condensed mathematical proof that the code is secure. In order to be applicable to global computers, the MOBIUS project will pioneer a PCC architecture that accommodates the distributed nature of global computing and allows enforcement of advanced policies, including both functional properties and advanced security properties such as non-interference or resource control. To ensure scalability, the MOBIUS project will also extend and combine two prime enabling technologies of PCC, ie type systems and program logics, and use the strength of these two techniques in hybrid certificates, to be verified through combined type checking and proof checking. Finally, the MOBIUS project will develop certificate translation as a means to bring to the code consumers the benefits of program verification, which is almost universally performed at source code level.

Modern verification environments based on program logics typically operate on source programs. The Mobius project proposes to combine these environments with type systems, which provide an automated means to enforce many basic policies, and use the resulting framework to cover a wide range of security policies for global computers. Evidence of programs adherence to their policy will be recorded by certificates: condensed, easily checkable formal proofs. In order to bring the benefits of source code verification to the code consumers, compilers will be enhanced to transform specifications and proofs for bytecode programs, yielding certificates that establish the correctness of bytecode programs and can be checked efficiently by code consumers.

To maximize its impact, the MOBIUS project is focusing on Java-enabled global computers, and uses program logics that support the Java Modelling Language (JML). It will allow an implementation of the MOBIUS security architecture to be built on top of existing tools developed within the consortium. This will be evaluated on case studies from a range of application domains, covered by the consortium industrial partners, and by the End User Panel.

The project is coordinated by the French research institute INRIA, and is part of the pro-active initiative Global Computing 2, launched by the Future and Emerging Technologies unit of the IST programme.

Link:
Project web site: http://mobius.inria.fr

Please contact:
Gilles Barthe, Project coordinator:
Tel: +33 4 92 38 79 38
E-mail: Gilles.Barthesophia.inria.fr