e-Science logo
About NeSC
e-Science Institute
e-Science Hub
e-Science Events
Presentations & Lectures
Technical Papers
Global Grid Links
UK e-Science Centres
UK e-Science Teams
Career Opportunities
Bibliographic Database


Mobile Resource Guarantees



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

These certificates will be condensed and formalised mathematical proofs of a resource-related property which are by their very nature self-evident and unforgable (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 Rubiks 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.
MRG (project IST-2001-33149) is funded by the European Commission under the FET proactive initiative on Global Computing. Project partners are the University of Edinburgh (coordinator) and Ludwig-Maximilians-Universität München.

Maturity: Initial Research
Region: EU
Type: International
Grant Value:
Start Date: 01/01/2002
End Date: 31/12/2004
Project Status: completed
Funding Agency: EU

Project Members
Prof Don Sannella

Collaborating Organisations
Ludwig-Maximilians-Universität München
School of Physics (University of Edinburgh)

Component(s) Project Develops
This project is not associated with any components at present.

Application Area(s) associated with Project
This project is not associated with any application areas at present.


Last Updated: 22 Jun 12 11:02
This is an archived website, preserved and hosted by the School of Physics and Astronomy at the University of Edinburgh. The School of Physics and Astronomy takes no responsibility for the content, accuracy or freshness of this website. Please email webmaster [at] ph [dot] ed [dot] ac [dot] uk for enquiries about this archive.