Abstract
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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Aspinall, D., Beringer, L., Hofmann, M., Loidl, H.-W., Momigliano, A.: A program logic for resource verification. In: Slind, K., Bunker, A., Gopalakrishnan, G.C. (eds.) TPHOLs 2004. LNCS, vol. 3223, pp. 34–49. Springer, Heidelberg (2004)
Aspinall, D., Beringer, L., Hofmann, M., Loidl, H.-W., Momigliano, A.: A program logic for resources. Technical Report EDI-INF-RR-0296, Informatics, University of Edinburgh (July 2005)
Aspinall, D., Beringer, L., Momigliano, A.: Optimisation validation. Technical report, Informatics, University of Edinburgh (December 2005)
Aspinall, D., Gilmore, S., Hofmann, M., Sannella, D., Stark, I.: Mobile resource guarantees for smart devices. In: Barthe, G., Burdy, L., Huisman, M., Lanet, J.-L., Muntean, T. (eds.) CASSIS 2004. LNCS, vol. 3362, pp. 1–26. Springer, Heidelberg (2005)
Bollella, G., et al.: The Real-time Specification for Java. Addison-Wesley, Reading (2000)
Beringer, L., Hofmann, M., Momigliano, A., Shkaravska, O.: Automatic certification of heap consumption. In: Baader, F., Voronkov, A. (eds.) LPAR 2004. LNCS (LNAI), vol. 3452, pp. 347–362. Springer, Heidelberg (2005)
Binder, W., Hulaas, J.G., Villazón, A.: Portable resource control in Java. In: OOPSLA 2001: Proceedings of the 16th ACM SIGPLAN conference on Object oriented programming, systems, languages, and applications, pp. 139–155. ACM Press, New York (2001)
Beringer, L., MacKenzie, K., Stark, I.: Grail: a functional form for imperative mobile code. Electronic Notes in Theoretical Computer Science 85(1) (June 2003)
Barthe, G., Pavlova, M., Schneider, G.: Precise analysis of memory consumption using program logics. In: Aichernig, B., Beckert, B. (eds.) Proceedings of SEFM 2005. IEEE Press, Los Alamitos (2005)
Campbell, B.: Folding stack memory usage prediction into heap. In: Proceedings of Quantitative Aspects of Programming Languages Workshop, ETAPS 2005 (April 2005)
Chander, A., Espinosa, D., Islam, N.: Enforcing resource bounds via static verification of dynamic checks. In: Sagiv, M. (ed.) ESOP 2005. LNCS, vol. 3444, pp. 311–325. Springer, Heidelberg (2005)
Czajkowski, G., Hahn, S., Skinner, G., Soper, P., Bryce, C.: Sun Microsystems. Technical Report TR-2003-124: A resource management interface for the Java platform (May 2003)
Czajkowski, G., von Eicken, T.: JRes: a resource accounting interface for Java. In: OOPSLA 1998: Proceedings of the 13th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, pp. 21–35. ACM Press, New York (1998)
Crary, K., Weirich, S.: Resource bound certification. In: Proc. 27th Symp. Principles of Prog. Lang. (POPL), pp. 184–198. ACM, New York (2000)
Gilmore, S., Prowse, M.: Proof-carrying bytecode. In: Proceedings of First Workshop on Bytecode Semantics, Verification, Analysis and Transformation (BYTECODE 2005), Edinburgh, Scotland (April 2005)
Hofmann, M., Jost, S.: Static prediction of heap space usage for firstorder functional programs. In: Proceedings of the 30th ACM Symposium on Principles of Programming Languages. ACM SIGPLAN Notices, vol. 38, pp. 185–197. ACM Press, New York (2003)
Hughes, J., Pareto, L.: Recursion and dynamic data structures in bounded space: towards embedded ML programming. In: Proc. International Conference on Functional Programming (ACM), Paris (September 1999)
J-S. J-SEAL2 website. See, www.jseal2.com
Hughes, J., Pareto, L.: Recursion and dynamic data structures in bounded space: towards embedded ML programming. In: Proc. International Conference on Functional Programming (ACM), Paris (September 1999)
MacKenzie, K., Wolverson, N.: Camelot and grail: resourceaware functional programming on the JVM. Trends in Functional Programing 4, 29–46 (2004); Intellect
Necula, G.C.: Compiling with Proofs. PhD thesis, Carnegie Mellon University (October 1998); Available as Technical Report CMU-CS-98-154
Talpin, J.-P., Jouvelot, P.: The type and effect discipline. Inf. Comput. 111(2), 245–296 (1994)
Vasconcelos, P., Hammond, K.: Inferring cost equations for recursive, polymorphic and higher-order functional programs. In: Trinder, P., Michaelson, G.J., Peña, R. (eds.) IFL 2003. LNCS, vol. 3145, pp. 86–101. Springer, Heidelberg (2004)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Aspinall, D., MacKenzie, K. (2006). Mobile Resource Guarantees and Policies. In: Barthe, G., Grégoire, B., Huisman, M., Lanet, JL. (eds) Construction and Analysis of Safe, Secure, and Interoperable Smart Devices. CASSIS 2005. Lecture Notes in Computer Science, vol 3956. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11741060_2
Download citation
DOI: https://doi.org/10.1007/11741060_2
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-33689-1
Online ISBN: 978-3-540-33691-4
eBook Packages: Computer ScienceComputer Science (R0)