USENIX Conference Policies
Model Checking of Multi-Applet JavaCard Applications
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.
BibTeX
@inproceedings {270467,
author = {Gennady Chugunov and Lars-{\r A}ke Fredlund and Dilian Gurov},
title = {Model Checking of {Multi-Applet} {JavaCard} Applications},
booktitle = {5th Smart Card Research and Advanced Application Conference (CARDIS 02)},
year = {2002},
address = {San Jose, CA},
url = {https://www.usenix.org/conference/cardis-02/model-checking-multi-applet-javacard-applications},
publisher = {USENIX Association},
month = nov
}
author = {Gennady Chugunov and Lars-{\r A}ke Fredlund and Dilian Gurov},
title = {Model Checking of {Multi-Applet} {JavaCard} Applications},
booktitle = {5th Smart Card Research and Advanced Application Conference (CARDIS 02)},
year = {2002},
address = {San Jose, CA},
url = {https://www.usenix.org/conference/cardis-02/model-checking-multi-applet-javacard-applications},
publisher = {USENIX Association},
month = nov
}