SawjaCard: A Static Analysis Tool for Certifying Java Card Applications

Frédéric Besson 1 Thomas Jensen 1 Pierre Vittet 1
1 CELTIQUE - Software certification with semantic analysis
Inria Rennes – Bretagne Atlantique , IRISA-D4 - LANGAGE ET GÉNIE LOGICIEL
Abstract : This paper describes the design and implementation of a static analysis tool for certifying Java Card applications, according to security rules defined by the smart card industry. Java Card is a dialect of Java designed for programming multi-application smart cards and the tool, called SawjaCard, has been specialised for the particular Java Card programming patterns. The tool is built around a static analysis engine which uses a combination of numeric and heap analysis. It includes a model of the Java Card libraries and the Java Card firewall. The tool has been evaluated on a series of industrial applets and is shown to au-tomate a substantial part of the validation process.
Type de document :
Communication dans un congrès
21st International Static Analysis Symposium (SAS 2014), 2014, Munich, Germany. Springer, 8858, pp.51 - 67, 2014, 〈10.1007/978-3-319-10936-7_4〉
Liste complète des métadonnées

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

https://hal.inria.fr/hal-01093327
Contributeur : Frédéric Besson <>
Soumis le : mercredi 10 décembre 2014 - 15:11:04
Dernière modification le : vendredi 16 novembre 2018 - 01:38:37
Document(s) archivé(s) le : mercredi 11 mars 2015 - 11:15:56

Fichier

sawjacard.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Citation

Frédéric Besson, Thomas Jensen, Pierre Vittet. SawjaCard: A Static Analysis Tool for Certifying Java Card Applications. 21st International Static Analysis Symposium (SAS 2014), 2014, Munich, Germany. Springer, 8858, pp.51 - 67, 2014, 〈10.1007/978-3-319-10936-7_4〉. 〈hal-01093327〉

Partager

Métriques

Consultations de la notice

2169

Téléchargements de fichiers

167