The paper proposes a framework for automatic model checking of temporal constraints on inter-applet communications in multi-applet JavaCards. The framework has been realised by combining a class-based static analysis tool with an automatic model checker for pushdown system and linear temporal logic.
In the future we will refine the static analysis to permit the analysis of communication capabilities of single applets thus connecting to the work on compositional proof systems for JavaCard applets suggested in [1]. This will permit us to analyse whether an applet can operate safely on a smart card even when the knowledge about other applets on the card is imperfect.
Further information regarding the model checking framework
and the availability of the tool components
and examples can be obtained at
the web location http://www.sics.se/fdt/projects/VeriCode/.