Abstract
We consider a scenario where (functional) programs in pre-compiled form are exchanged among untrusted parties. Our contribution is a system of annotations for the code that can be verified at load time so as to ensure bounds on the time and space resources required for its execution, as well as to guarantee the usual integrity properties.
Specifically, we define a simple stack machine for a first-order functional language and show how to perform type, size, and termination verifications at the level of the bytecode of the machine. In particular, we show that a combination of size verification based on quasi-interpretations and of termination verification based on lexicographic path orders leads to an explicit bound on the space required for the execution.
This work was partly supported by ACI Sécurité Informatique, project CRISS.
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
Abadi, M., Stata, R.: A type system for Java bytecode subroutines. In: Proc. POPL (1998)
Amadio, R.: Max-plus quasi-interpretations. In: Hofmann, M.O. (ed.) TLCA 2003. LNCS, vol. 2701, Springer, Heidelberg (2003)
Amadio, R., Coupet-Grimal, S., Zilio, S.D., Jakubiec, L.: A functional scenario for bytecode verification of resource bounds. Research Report LIF 17-2004 (2004)
Bellantoni, S., Cook, S.: A new recursion-theoretic characterization of the poly-time functions. Computational Complexity 2, 97–110 (1992)
Bonfante, G., Marion, J.-Y., Moyen, J.-Y.: On termination methods with space bound certifications. In: Bjørner, D., Broy, M., Zamulin, A.V. (eds.) PSI 2001. LNCS, vol. 2244, Springer, Heidelberg (2001)
Baader, F., Nipkow, T.: Term rewriting and all that. Cambridge University Press, Cambridge (1998)
Cobham, A.: The intrinsic computational difficulty of functions. In: Proc. Logic,Methodology, and Philosophy of Science II. North Holland, Amsterdam (1965)
Hofmann, M.: The strength of non size-increasing computation. In: Proc. POPL (2002)
Jones, N.: Computability and complexity, from a programming perspective. MIT Press, Cambridge (1997)
Kildall, G.: A unified approach to global program optimization. In: Proc. POPL (1973)
Leivant, D.: Predicative recurrence and computational complexity i: word recurrence and poly-time. In: Clote, Remmel (eds.) Feasible mathematics II, Birkhäuser (1994)
Lindholm, T., Yellin, F.: The Java virtual machine specification. Addison-Wesley, Reading (1999)
Marion, J.-Y.: Complexité implicite des calculs, de la théorie à la pratique. Habilitation à diriger des recherches, Université de Nancy (2000)
Marion, J.-Y., Moyen, J.-Y.: Termination and resource analysis of assembly programs by Petri Nets. Technical Report, Université de Nancy (2003)
Morriset, G., Walker, D., Crary, K., Glew, N.: From system F to typed assembly language. ACM Transactions on Programming Languages and Systems 21(3), 528–569 (1999)
Necula, G.: Proof carrying code. In: Proc. POPL (1997)
Sannella, D.: Mobile resource guarantee. In: IST-Global Computing research proposal, U. Edinburgh (2001), http://www.dcs.ed.ac.uk/home/mrg/
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Amadio, R.M., Coupet-Grimal, S., Dal Zilio, S., Jakubiec, L. (2004). A Functional Scenario for Bytecode Verification of Resource Bounds. In: Marcinkowski, J., Tarlecki, A. (eds) Computer Science Logic. CSL 2004. Lecture Notes in Computer Science, vol 3210. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-30124-0_22
Download citation
DOI: https://doi.org/10.1007/978-3-540-30124-0_22
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-23024-3
Online ISBN: 978-3-540-30124-0
eBook Packages: Springer Book Archive