Smart cards have come to play an ever increasing role in our lives. We use them in electronic banking, to keep health care data, for mobile telephony, and in many other applications. The most important aspect of smartcards is their security; users and card issuers have to agree that the level of security provided by a smartcard platform is enough to prevent malicious agents from abusing their trust in a card application.
Since the number of smartcard applications is growing rapidly, it is natural to provide smartcards with the possibility of accommodating multiple applications, and the possibility to delete or add new applications after the card has been issued. Furthermore, such multi-application smartcards allow partner applications to cooperate and exchange data. Popular applications of multi-application cards are partner loyalty programs, mobile telephone to banking partnership programs, etc. The JavaCard platform [12] is one platform for building such multi-application smartcards. It is based on a subset of Java tailored to the task of embedding on a smartcard. The current standard omits many of the features of Java such as concurrency through threads, garbage collection, and many API functions but has a notion of applets to support multiple applications.
One important aspect which distinguishes multi-applet JavaCards from single-applet ones is the support for inter-applet communication via method calls. Communication naturally comes at a price: applets must guard against illicit invocations of their public methods from unwarranted applets, and from leakage of data to third parties. Even if a multi-applet application were to be proved safe, there still exists the possibility of new unsafe applets being loaded onto the card post-verification. The JavaCard platform provides features to partially address these security concerns. Apart from a Java-style byte code verifier, which in the current generation of JavaCard smartcards is typically located off-card, there is a concept of a communication firewall that by default prohibits applets from communicating with each other. To enable communication to flow between applets, a recipient applet has to explicitly permit calls from the caller applet.
Such checks as above are static in nature, e.g., method calls are always allowed, or they are never allowed. The work reported here in contrast permits to begin to characterise the temporal restrictions of inter-applet communications. In the formulation of such restrictions we consider a situation when a set of applets have been loaded onto a smartcard, and formulate properties in Linear Temporal Logic (LTL) regarding inter-applet communications (in addition to properties about intra-applet method calls and API usage).
To provide a semantic bridge between multi-applet programs and the temporal logic specification language, we use the abstract notion of a program graph, capturing the control flow of programs with procedures/methods, and which can be efficiently computed. The behaviour of such program graphs is defined through the notion of pushdown systems, which provide a natural execution model for programs with methods (and possibly recursion), and for which completely automatic model checkers for LTL exist.
In more detail the model checking proceeds as follows. First the method call graphs of a set of JavaCard applets are obtained using a Java byte code analysis tool [13] developed at INRIA Rennes, which we have adapted for JavaCard. The analysis is performed on a class basis. As a consequence individual applet instances cannot be reasoned about; correctness properties concern activation of methods of classes extending the JavaCard Applet class, rather than activation of methods of an applet instance. Further details and limitations of this static analysis procedure are discussed in Section 2.
The resulting method call graphs are translated into pushdown systems, a natural execution model for programs with recursion. Essentially a pushdown system is a pair of a control location with a stack of stack symbols. In our encoding we use a single control location and let the stack symbols represent the program points of the underlying JavaCard applets. The details of the translation are elaborated in Section 3.1.
For pushdown systems the model checking procedure for Linear Temporal Logic (LTL) is decidable and of polynomial complexity in the size of the system [3,9,7]. The atomic predicates of the logic, tailored to JavaCard, are the program points themselves and predicates expressing class and package membership of program points. The Moped model checker [8] is used to check LTL properties of pushdown systems. Sections 3.2,3.3 and 3.4 describes the logic and our use of the Moped tool in further detail.
To motivate and demonstrate our approach we have selected a prototypical JavaCard example: a purse applet stores money, and interacts with loyalty applets on receiving a purchase order. A loyalty applet can have agreements with other applets, and can thus in turn communicate with another applet on receiving information about a purse transaction. In Section 4 we demonstrate the effectiveness of our approach in analysing such inter-applet communication patterns.
There exists by now a growing number of related work concerning model checking Java (or JavaCard), or more general formal analysis of JavaCard applications; below we will mention a few of them.
The Compaq Extended Static Checker for Java (ESC/Java) [14], developed at the Compaq Systems Research Center (SRC), is a programming tool for finding errors in Java programs. ESC/Java includes an annotation language with which programmers can express design decisions using light-weight specifications. Checking is neither sound nor complete, but can yield informative warning messages2. A case study in the context of JavaCard, based on the Gemplus purse applet, is presented in [5].
The first version of the Java PathFinder [10], JPF, was a translator from a subset of Java 1.0 to PROMELA, the programming language of the Spin model checker. A similar translator tool from Java to PROMELA (actually the variant of PROMELA for the dSpin tool) is reported in [11]. The Java Pathfinder tool is especially suited for analyzing multi-threaded Java applications, where normal testing usually falls short. The tool can find deadlocks and violations of boolean assertions stated by the programmer in a special assertion language. A second version of the tool reportedly works directly on bytecode and has support for garbage collection3.
The Bandera Project [6] aims to develop techniques and tools for automated reasoning about Java based software system behavior, and to apply these tools to construct high-confidence mission-critical software. Automated reasoning is achieved by (1) mechanically creating high-level models of software systems using abstract interpretation and partial evaluation technologies, and then (2) employing model-checking techniques to automatically verify that software specifications are satisfied by the model4.
In [2] an approach is presented for checking properties of multi-applet interactions of JavaCards based on associating security levels to applets and applet data, and to thus detect illegal flow of information between applets. Technically the approach requires building abstract models by hand from byte code, and then to check them automatically using the SMV model checker.
Our work is related to the program verification approach of [13] which is based on method call graphs. The operational semantics of the graphs, however, is given there directly through a set of transition rules (rather than through pushdown systems), and security properties are expressed as call-stack invariants. Following a similar program representation, a compositional account is given in [1], where a compositional proof system for inferring temporal properties of a multi-applet program from the properties of the individual applets is presented.