Java bytecode verification: algorithms and formalizations

Abstract : Bytecode verification is a crucial security component for Java applets, on the Web and on embedded devices such as smart cards. This paper reviews the various bytecode verification algorithms that have been proposed, recasts them in a common framework of dataflow analysis, and surveys the use of proof assistants to specify bytecode verification and prove its correctness.
Type de document :
Article dans une revue
Journal of Automated Reasoning, Springer Verlag, 2003, 30 (3-4), pp.235--269. 〈10.1023/A:1025055424017〉
Liste complète des métadonnées

Littérature citée [58 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01499939
Contributeur : Xavier Leroy <>
Soumis le : samedi 1 avril 2017 - 17:25:44
Dernière modification le : mardi 17 avril 2018 - 11:27:22
Document(s) archivé(s) le : dimanche 2 juillet 2017 - 12:57:49

Fichier

bytecode-verification-JAR.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

Xavier Leroy. Java bytecode verification: algorithms and formalizations. Journal of Automated Reasoning, Springer Verlag, 2003, 30 (3-4), pp.235--269. 〈10.1023/A:1025055424017〉. 〈hal-01499939〉

Partager

Métriques

Consultations de la notice

160

Téléchargements de fichiers

112