Verification of Java Card applets behavior with respect to transactions and card tears

Claude Marché 1, 2 Nicolas Rousset 1
1 PROVAL - Proof of Programs
UP11 - Université Paris-Sud - Paris 11, Inria Saclay - Ile de France, CNRS - Centre National de la Recherche Scientifique : UMR
2 LRI - Laboratoire de Recherche en Informatique
Abstract : The Java Card transaction mechanism allows to protect sensitive operations on smart cards against problems due to card tears or power losses. Statements within a transaction are viewed as a single atomic operation so that either they are all performed or none of them is. Krakatoa is a tool for static verification of Java programs annotated in JML (Java Modeling Language), a behavioral specification language tailored to Java and based on first order predicate logic. In a first step, we show how we modeled the transactions within Krakatoa, by generating on-the-fly (i.e. on each applet) specifications of the API methods for transactions. In a second step, we consider security problems that can be caused by a card tear. We propose new JML constructs allowing to express properties to satisfy when a method is interrupted by a card tear, also taking non-atomic methods into account. We present a modeling of these constructs in Krakatoa, and show it is practicable for the detection of potential security holes, or to prove the absence of risk.
Keywords : Formal verification JML Java Card applets Transactions Card Tears non-atomic methods
Type de document :
Communication dans un congrès
Dang Van Hung, Paritosh Pandya. Software Engineering and Formal Methods, Sep 2006, Pune, India. IEEE Comp. Soc. Press, 2006, th IEEE International Conference on Software Engineering and Formal Methods (SEFM'06)
Liste complète des métadonnées
https://hal.inria.fr/inria-00129055
Contributeur : Claude Marché <>
Soumis le : lundi 5 février 2007 - 15:44:09
Dernière modification le : jeudi 5 avril 2018 - 12:30:08

Identifiants

  • HAL Id : inria-00129055, version 1

Collections

INRIA | UMR8623

Citation

Claude Marché, Nicolas Rousset. Verification of Java Card applets behavior with respect to transactions and card tears. Dang Van Hung, Paritosh Pandya. Software Engineering and Formal Methods, Sep 2006, Pune, India. IEEE Comp. Soc. Press, 2006, th IEEE International Conference on Software Engineering and Formal Methods (SEFM'06). 〈inria-00129055〉

Exporter

BibTeX TEI DC DCterms EndNote

Partager

Métriques

Consultations de la notice

150

Contact


archive-ouverte@inria.fr