Computing stack maps with interfaces

Frédéric Besson 1 Thomas Jensen 1 Tiphaine Turpin 1
1 Lande - Logiciel : ANalyse et DEveloppement
IRISA - Institut de Recherche en Informatique et Systèmes Aléatoires, Inria Rennes – Bretagne Atlantique
Abstract : Lightweigth byte code verification uses stack maps to annotate Java byte code programs with type information so that the byte code verifier (BCV) only has to check this typing, without having to do any data flow analysis. This report describes an improved analysis technique together with algorithms for optimizing the stack maps generated by the analyser. The improved BCV is based on a modified version of the abstract domain. This domain is simplified in its treatment of base values, keeping only the necessary information to ensure the memory safety property. It is richer in its representation of interface types, using the known Dedekind-MacNeille completion technique to construct abstract domain elements representing sets of interfaces. Tracking interface information allows to remove the dynamic checks at interface method invocations. We prove the memory safety property guaranteed by BCV using an operational semantics whose distinguishing feature is a low-level memory model operating on untagged 32-bit values, as opposed to the standard, higher-level memory models using tagged memory objects. For bytecode that is typable without sets of types (this includes any code compiled from Java) we show how to prune the fix-point to obtain a stack map that can be validated without the interface set computations arising from this extension. In the context of lightweight verification, this is an advantage as it does not make the verification more complex or costly. The size of the certificates is not significantly modified. Experiments show that the pruning can be done by reasonably efficient (though in theory exponential) algorithms that uses heuristics to explore the space of valid program typings from the least fixpoint generated by the analyser. Stack maps for three substantial test suites were correctly handled by the optimized (but incomplete) pruning algorithm.
Type de document :
[Research Report] PI 1879, 2008, pp.39
Liste complète des métadonnées

Littérature citée [16 références]  Voir  Masquer  Télécharger
Contributeur : Anne Jaigu <>
Soumis le : mardi 15 juillet 2008 - 13:57:23
Dernière modification le : jeudi 11 janvier 2018 - 06:20:09
Document(s) archivé(s) le : mardi 21 septembre 2010 - 16:55:06


Fichiers produits par l'(les) auteur(s)


  • HAL Id : inria-00200724, version 2



Frédéric Besson, Thomas Jensen, Tiphaine Turpin. Computing stack maps with interfaces. [Research Report] PI 1879, 2008, pp.39. 〈inria-00200724v2〉



Consultations de la notice


Téléchargements de fichiers