Fourth IEEE International Conference on Software Engineering and Formal Methods (SEFM'06)
Verification of JAVA CARD Applets Behavior with Respect to Transactions and Card Tears
Pune, India
September 11-September 15
ISBN: 0-7695-2678-0
DOI Bookmark:
http://doi.ieeecomputersociety.org/10.1109/SEFM.2006.38
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.
Index Terms:
Formal verification, JML, JAVA CARD applets, Transactions, Card Tears, non-atomic methods.
Citation:
Claude Marche, Nicolas Rousset, "Verification of JAVA CARD Applets Behavior with Respect to Transactions and Card Tears," sefm, pp.137-146, Fourth IEEE International Conference on Software Engineering and Formal Methods (SEFM'06), 2006
Usage of this product signifies your acceptance of the
Terms of Use.
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb