| ||||||||||||||||||||||||||||||||||||||||||||||||||||
|
CARDIS '02 Paper
[CARDIS '02 Tech Program Index]
Next: Introduction
Model Checking of Multi-Applet JavaCard Applications1
Gennady Chugunov -
Lars-Åke Fredlund
-
Dilian Gurov
-
Abstract:
The paper describes a framework for model checking
JavaCard applets on the bytecode level.
From a set of JavaCard applets we extract their method call graphs
using a static analysis tool. The resulting structure
is translated into a pushdown system for which
the model checking problem for Linear Temporal Logic (LTL)
is decidable,
and for which there are efficient
model checking tools available.
The model checking approach of the paper is tailored
to the analysis of
inter applet (intra card) communications
and we demonstrate it using a prototypical example
of a purse applet and a set of loyalty applets.
Lars-Ake Fredlund 2002-09-23 |
|
This paper was originally published in the
Proceedings of the Fifth Smart Card Research and Advanced Application Conference,
November 21–22, 2002, San Jose, CA, USA
Last changed: 11 Oct. 2002 aw |
|
