Mobile Resource Guarantees

Don Sannella

(Edinburgh)

The Mobile Resource Guarantees (MRG) project is building infrastructure for endowing mobile bytecode programs with independently verifiable certificates describing their resource consumption. These certificates will be condensed and formalised mathematical proofs of a resource-related property which are by their very nature self-evident and unforgeable. Arbitrarily complex methods may be used to construct such a certificate, but once constructed its verification will always be a simple computation. This makes it feasible for the recipient to check that the proof is valid, and so the claimed property holds, before running the code. This work falls within an area known as "proof carrying code". Our focus in MRG on quantitative resource guarantees is different from the traditional PCC focus which is security. Another novelty is the method to be used to generate proofs, which is to use a "linear" type system that classifies programs according to their resource usage as well as according to the kinds of values they consume and produce. The intention is to generate proofs of resource usage from typing derivations. The MRG project (IST-2001-33149), which is a collaboration between the University of Edinburgh and LMU Munich, is funded by the EC under the FET proactive initiative on Global Computing.
Tuesday 18th November 2003, 14:00
Robert Recorde Room
Department of Computer Science