David Aspinall, Stephen Gilmore, Martin Hofmann, Donald Sannella and Ian Stark
In Construction and Analysis of Safe, Secure and Interoperable Smart Devices: Proceedings of the International Workshop CASSIS 2004, Marseille, France, March 10–14, 2004, Lecture Notes in Computer Science 3362, pages 1–26. Springer-Verlag, 2005.
Fetch paper. Go to other papers, talks or home page.
We present the Mobile Resource Guarantees framework: a system for ensuring that downloaded programs are free from run-time violations of resource bounds. Certificates are attached to code in the form of efficiently checkable proofs of resource bounds; in contrast to cryptographic certificates of code origin, these are independent of trust networks. A novel programming language with resource constraints encoded in function types is used to streamline the generation of proofs of resource usage.
@InProceedings{aspinall+:mrg-smart-devices,
author = {David Aspinall and Stephen Gilmore and Martin
Hofmann and Donald Sannella and Ian Stark},
title = {Mobile Resource Guarantees for Smart Devices},
booktitle = {Construction and Analysis of Safe, Secure and
Interoperable Smart Devices: Proceedings of the
International Workshop CASSIS~2004},
pages = {1--26},
year = 2005,
number = 3362,
series = {Lecture Notes in Computer Science},
publisher = {Springer-Verlag},
url = {http://www.inf.ed.ac.uk/~stark/mrg-smart-devices.html},
pdf = {http://www.inf.ed.ac.uk/~stark/mrg-smart-devices.pdf}
}
This research was supported by MRG, project IST-2001-33149 in the Future and Emerging Technologies proactive initiative on Global Computing, funded by the European Community Fifth Framework Programme.
Ian Stark was supported by EPSRC Advanced Research Fellowship GR/R76950/01 Mathematical Models for Concurrent and Mobile Computation.