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.