Vérification de bytecode Java Card

La vérification de bytecode dans les cartes à puces de type Java Card est aujourd'hui utilisée pour assurer la sécurité et l'intégrité des données. Le principal problème des Java Card repose sur le fait qu'une fois que nous possedons physique la carte à puce, n'importe quelle personne peut télécharger sur la carte à puce un ou plusieurs application hostile qui lui permettrait d'exploiter des failles de sécurités ou récupérer des données personnelles (personnelles, bancaire, etc...). Pour cela, des études et recherches ont été menées afin d'intégrer cela directement dans la carte à puce. Ce logiciel système peut ainsi utiliser des techniques de cryptographies afin d'assurer cette protection des données. De plus, cette vérification de bytecode peut aussi permettre d'éviter l'intégration d'un code malveillant lors de la programmation de la carte à puce.

Les outils disponibles

JaKarTa est un ensemble d'outils mis à disposition des développeurs afin de réaliser des spécifications pour assurer la sécurité et l'intégrité des données dès que le programme développé sera ajouté et utilisé par la Java Card. Cette ensemble d'outils, implémenté en Objective Caml se décompose en 4 catégories :

• Jakarta Specification Language (JSL), permettant d'écrire des exécutables de spécifications lisibles.
• Jakarta Transformation Kit (JTK), permettant de transformer et manipuler les spécifications JSL.
• Jakarta Prover Interface (JPI), permettant de compiler les spécifications JSL en assistant de preuves.
• Jakarta Automation Kit (JAK),…

Articles scientifiques

• (en) Chi YaPing, Li ZhaoBin, Fang Yong et Wang ZhongHua, « An Improved Bytecode Verification Algorithm on Java Card », Computational Intelligence and Security, 2009. CIS '09. International Conference on, IEEE,‎ 11-14 decembre 2009, p. 552-555 (ISBN 978-1-4244-5411-2, DOI 10.1109/CIS.2009.193)
• (en) Ludovic Casset et Jean-Louis Lannet, « Increasing smart card dependability », Proceeding EW 10 Proceedings of the 10th workshop on ACM SIGOPS European workshop, ACM,‎ NC nc 2002, p. 209-212 (ISBN NC^{[à vérifier : ISBN invalide]}, DOI 10.1145/1133373.1133416)
• (en) Ludovic Casset, Lilian Burdy et Antoine Requet, « Formal Development of an Embedded Verifier for Java Card Byte Code », Dependable Systems and Networks, 2002. DSN 2002. Proceedings. International Conference on, IEEE,‎ 10 décembre 2002, p. 51-56 (ISBN 0-7695-1101-5, DOI 10.1109/DSN.2002.1028886)
• (en) G. Barthe, G. Dufay, M. Huisman et S. Melo De Sousa, « In Smart Card Programming and Security, International Conference on Research in Smart Cards, e-Smart 2001 », NC, Springer-Verlag,‎ 19-21 septembre 2001, p. 2-18 (ISBN 3540426108, DOI NC)

• (en) Xavier Leroy, « Bytecode verification on Java smart cards », Software: Practice and Experience, John Wiley & Sons, Ltd.,‎ 15 mars 2002, p. 319-340 (ISBN NC^{[à vérifier : ISBN invalide]}, DOI 10.1002/spe.438)

• (en) Xavier Leroy, « On-Card Bytecode Verification for Java Card », Lecture Notes in Computer Science, SpringerLink,‎ NC nc 2001, p. 150-164 (ISBN NC^{[à vérifier : ISBN invalide]}, DOI 10.1007/3-540-45418-7_13)

Liens externes

• Adding reliability and trust to smartcards de l'ICT Results - Cordis - VerifiCard's Jakarta
• VefiriCard's Project INRIA's homepage for the IST-funded project VerifiCard