Mobile Resource Guarantees for Smart Devices

D Aspinall*, S Gilmore, M Hofmann, D Sannella, I Stark

*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

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.

Original languageEnglish
Title of host publicationConstruction and Analysis of Safe, Secure, and Interoperable Smart Devices
Subtitle of host publicationInternational Workshop, CASSIS 2004, Marseille, France, March 10-14, 2004, Revised Selected Papers
EditorsGilles Barthe, Lilian Burdy, Marieke Huisman, Jean-Louis Lanet, Traian Muntean
Place of PublicationBerlin
PublisherSpringer-Verlag GmbH
Pages1-26
Number of pages26
Volume3362
ISBN (Electronic)978-3-540-30569-9
ISBN (Print)978-3-540-24287-1
DOIs
Publication statusPublished - 2005
EventInternational Workshop on Construction and Analysis of Safe, Secure, and Interoperable Smart Devices - Marseille, France
Duration: 10 Mar 200414 Mar 2004

Publication series

NameLecture Notes in Computer Science
PublisherSpringer Berlin / Heidelberg
Volume3362
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

ConferenceInternational Workshop on Construction and Analysis of Safe, Secure, and Interoperable Smart Devices
CountryFrance
CityMarseille
Period10/03/0414/03/04

Keywords

  • verification

Cite this