Abstract
We present a certified algorithm for resource usage analysis, applicable to languages in the style of Java byte code. The algorithm verifies that a program executes in bounded memory. The algorithm is destined to be used in the development process of applets and for enhanced byte code verification on embedded devices. We have therefore aimed at a low-complexity algorithm derived from a loop detection algorithm for control flow graphs. The expression of the algorithm as a constraint-based static analysis of the program over simple lattices provides a link with abstract interpretation that allows to state and prove formally the correctness of the analysis with respect to an operational semantics of the program. The certification is based on an abstract interpretation framework implemented in the Coq proof assistant which has been used to provide a complete formalisation and formal verification of all correctness proofs.
This work was partially supported by the French RNTL project ”Castles”.
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., Compagnoni, A.: Heap bounded assembly language. Journal of Automated Reasoning 31(3–4), 261–302 (2003)
Barthe, G., Dufay, G., Jakubiec, L., Serpette, B., de Sousa, S.M.: A Formal Executable Semantics of the JavaCard Platform. In: Sands, D. (ed.) ESOP 2001. LNCS, vol. 2028, p. 302. Springer, Heidelberg (2001)
Cachera, D., Jensen, T., Pichardie, D., Rusu, V.: Extracting a data flow analyser in constructive logic. In: Schmidt, D. (ed.) ESOP 2004. LNCS, vol. 2986, pp. 385–400. Springer, Heidelberg (2004)
Casset, L., Burdy, L., Requet, A.: Formal Development of an embedded verifier for Java Card Byte Code. In: Proc. of IEEE Int. Conference on Dependable Systems & Networks (DSN) (2002)
Crary, K., Weirich, S.: Resource bound certification. In: Proc. 27th ACM Symp. on Principles of Programming Languages (POPL 2000), pp. 184–198. ACM Press, New York (2000)
Filliâtre, J.-C., Marché, C.: Multi-Prover Verification of C Programs. In: Davies, J., Schulte, W., Barnett, M. (eds.) ICFEM 2004. LNCS, vol. 3308, pp. 15–29. Springer, Heidelberg (2004)
Hofmann, M.: A type system for bounded space and functional in-place update. Nordic Journal of Computing 7(4), 258–289 (2000)
Hofmann, M., Jost, S.: Static prediction of heap space usage for first-order functional programs. In: Proc. of 30th ACM Symp. on Principles of Programming Languages (POPL 2003), pp. 185–197. ACM Press, New York (2003)
Klein, G., Nipkow, T.: Verified Bytecode Verifiers. Theoretical Computer Science 298(3), 583–626 (2002)
Leroy, X.: On-card bytecode verification for Java card. In: Attali, S., Jensen, T. (eds.) E-smart 2001. LNCS, vol. 2140, pp. 150–164. Springer, Heidelberg (2001)
Marlet, R.: Syntax of the JCVM language to be studied in the SecSafe project. Technical Report SECSAFE-TL-005, Trusted Logic SA (May 2001)
Morrisett, G., Walker, D., Crary, K., Glew, N.: From System F to typed assembly language. ACM Trans. Program. Lang. Syst. 21(3), 527–568 (1999)
Pichardie, D.: Coq sources of the development, http://www.irisa.fr/lande/pichardie/MemoryUsage/
Schneider, G.: A constraint-based algorithm for analysing memory usage on Java cards. Technical Report RR-5440, INRIA (December 2004)
Siveroni, I.: Operational semantics of the Java Card Virtual Machine. J. Logic and Algebraic Programming 58(1-2) (2004)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Cachera, D., Jensen, T., Pichardie, D., Schneider, G. (2005). Certified Memory Usage Analysis. In: Fitzgerald, J., Hayes, I.J., Tarlecki, A. (eds) FM 2005: Formal Methods. FM 2005. Lecture Notes in Computer Science, vol 3582. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11526841_8
Download citation
DOI: https://doi.org/10.1007/11526841_8
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-27882-5
Online ISBN: 978-3-540-31714-2
eBook Packages: Computer ScienceComputer Science (R0)