A constraint-based algorithm for analysing memory usage on Java cards

Gerardo Schneider 1
1 Lande - Logiciel : ANalyse et DEveloppement
IRISA - Institut de Recherche en Informatique et Systèmes Aléatoires, Inria Rennes – Bretagne Atlantique
Abstract : We address in this paper the problem of statically determining whether a JavaCard applet may produce a memory overflow because of the dynamic instantiation of classes inside cycles. We provide a constraint-based algorithm which determines potential loops and (mutually) recursive methods. The algorithm operates on the byte-code of an applet. It is written as a set of rules -one for each byte-code instruction- which allows a compositional reasoning and it comprises both inter- and intra-procedural analysis. We aimed at an algorithm suitable to be fed into the proof assistant Coq in order to extract a certified memory usage analyser. We prove termination of the algorithm as well as its soundness and completeness with respect to an abstraction of the operational semantics of the language.
Document type :
Reports
Complete list of metadatas

https://hal.inria.fr/inria-00070567
Contributor : Rapport de Recherche Inria <>
Submitted on : Friday, May 19, 2006 - 8:53:52 PM
Last modification on : Friday, November 16, 2018 - 1:22:14 AM
Long-term archiving on : Sunday, April 4, 2010 - 9:28:59 PM

Identifiers

  • HAL Id : inria-00070567, version 1

Citation

Gerardo Schneider. A constraint-based algorithm for analysing memory usage on Java cards. [Research Report] RR-5440, INRIA. 2004, pp.26. ⟨inria-00070567⟩

Share

Metrics

Record views

162

Files downloads

167