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 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.

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.


Professor Donald Sannella
Laboratory for Foundations of Computer Science
School of Informatics
University of Edinburgh
Edinburgh EH9 3JZ, +44 131 650 5184 (direct line), +44 131 667 7209 (fax)