Mobile Resource Guarantees and Policies

David Aspinall, Kenneth MacKenzie

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


This paper introduces notions of resource policy for mobile code to be run on smart devices, to integrate with the proof-carrying code architecture of the Mobile Resource Guarantees (MRG) project. Two forms of policy are used: guaranteed policies which come with proofs and target policies which describe limits of the device. A guaranteed policy is expressed as a function of a methods input sizes, which determines a bound on consumption of some resource. A target policy is defined by a constant bound and input constraints for a method. A recipient of mobile code chooses whether to run methods by comparing between a guaranteed policy and the target policy. Since delivered code may use methods implemented on the target machine, guaranteed policies may also be provided by the platform; they appear symbolically as assumptions in delivered proofs. Guaranteed policies entail proof obligations that must be established from the proof certificate. Before proof, a policy checker ensures that the guaranteed policy refines the target policy; our policy format ensures that this step is tractable and does not require proof. Delivering policies thus mediates between arbitrary target requirements and the desirability to package code and certificate only once.
Original languageEnglish
Title of host publicationMobile Resource Guarantees and Policies
Subtitle of host publicationConstruction and Analysis of Safe, Secure, and Interoperable Smart Devices
EditorsGilles Barthe, Benjamin Grégoire, Marieke Huisman, Jean-Louis Lanet
PublisherSpringer Berlin Heidelberg
Number of pages21
ISBN (Electronic)978-3-540-33691-4
ISBN (Print)978-3-540-33689-1
Publication statusPublished - 2006

Publication series

NameLecture Notes in Computer Science
PublisherSpringer Berlin Heidelberg
ISSN (Print)0302-9743

Cite this