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,
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.
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
- 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.
Prof Don Sannella
|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 10:56
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.