MRG Project Logo

Mobile Resource Guarantees
(MRG, project IST-2001-33149)

The MRG project was funded in 2002-2005 under the Global Computing pro-active initiative of the Future and Emerging Technologies part of the Information Society Technologies programme of the European Commission's Fifth Framework Programme.

Home
Summary
Gallery
Site Map
People
Publications
Camelot
Internal
Related Projects
Admin

Summary

The Mobile Resource Guarantees (MRG) project has developed the infrastructure needed to endow mobile code with independently verifiable certificates describing its resource behaviour (space, time, etc.).

These certificates are condensed and formalised mathematical proofs of a resource-related property which are by their very nature self-evident and unforgeable (proof-carrying code). Arbitrarily complex methods may be used by the code producer to construct these certificates, but their verification by the code consumer will always be a simple computation. One may compare this to the verification of alleged solutions to combinatorial problems such as Rubik's cube or the travelling salesman problem.

One way that a code producer may produce proofs of resource bounds is by using a programming language equipped with a linear resource-aware type system, whereby programs are certified by virtue of their typing as satisfying certain resource bounds. A corresponding proof at the bytecode level can be generated automatically from a typing derivation in such a system in the course of compiling the program to bytecode.

Scenarios of application for the proposed framework include the following.

  • A provider of distributed computational power may only be willing to offer this service upon receiving dependable guarantees about the required resource consumption.

  • A user of a handheld device, wearable computer, or smart card might want to know that a downloaded application will definitely run within the limited amount of memory available.

  • Third-party software updates for mobile phones, household appliances, or car electronics should come with a guarantee not to set system parameters beyond manufacturer-specified safe limits.

  • Requiring certificates of specified resource consumption will also help to prevent mobile agents from performing denial of service attacks using bona fide host environments as a portal.

See also


Google
www groups.inf.ed.ac.uk
These pages are hosted by the Informatics Groups server at the University of Edinburgh.
Site maintained by Robert Atkey. This page last updated on: 2005-10-12.

Valid HTML 4.01!
Validate this page