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
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.
Complete list of metadatas
Contributor : Claude Marché <>
Submitted on : Monday, February 5, 2007 - 3:44:09 PM
Last modification on : Thursday, April 5, 2018 - 12:30:08 PM


  • HAL Id : inria-00129055, version 1



Claude Marché, Nicolas Rousset. Verification of Java Card applets behavior with respect to transactions and card tears. Software Engineering and Formal Methods, Sep 2006, Pune, India. ⟨inria-00129055⟩



Record views