Mobile Resource Guarantees and Policies

9 years 7 months ago
Mobile Resource Guarantees and Policies
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 th...
David Aspinall, Kenneth MacKenzie
Added 26 Jun 2010
Updated 26 Jun 2010
Type Conference
Year 2005
Authors David Aspinall, Kenneth MacKenzie
Comments (0)