Java Card provides a framework of classes and interfaces that hide the details of the underlying smart card interface and make it possible to load and run on the same card several applets, from different application providers with complex trust relationships. This fact paves the way for new business applications, but the card issuer has to secure absence of malicious or faulty card applets. He has to be able to check that (i) applets do not cause illicit method invocations that violate temporal restrictions of inter-applet communication, (ii) applets protect themselves from unwanted information flow to third parties and (iii) it is not possible for an unhandled Java Card API exception to leave an applet in an unpredictable state that is potentially dangerous for the application’s security. The authors explore recent advances in theory and tool support of static program analysis and they present an approach for automatic verification of smart card applications that by definition are security critical.
TopIntroduction
In this work, we propose program analysis techniques implemented in the FindBugs open source framework (Hovemeyer & Pugh, 2004; The FindBugs project site, 2009), for statically verifying important security properties of interacting Java Card applets.
Static program analysis has the potential to become a credible technique for automatic verification of smart card applications that by definition are security critical. There is a large collection of well established analysis techniques and recent research developments, as well as versatile analysis frameworks like FindBugs that open excellent prospects to exploit the provided support and the already implemented error detectors. Current article introduces error detectors adapted to the security requirements of the Java Card multi-applet environment, in order to highlight the perspectives and the limitations of the discussed alternative.
The most significant virtue is the use of a single verification technique, in place of existing verification approaches that require highly specialized formal analysis skills, for the different Java Card security verification tasks. In our case, analysis assumes only basic Java programming skills, but the analysis precision is restricted by the current limitations of the analysis support provided by FindBugs. We highlight these limitations and we discuss recent research work that aims at improved analysis precision, based on requirements that may be fulfilled in future versions of FindBugs.
Our analysis addresses the security concerns caused by the fact that Java Card allows several applets to load and run on the same card, from different application providers with complex trust relationships and partnerships. The Java Card platform controls cooperation of interacting applets through a firewall mechanism that enforces applet isolation and allows communication only through explicitly declared shareable interfaces including the explicitly permitted method invocations. This sort of checks is static in nature, i.e. one method call is either allowed in all cases or it is never allowed. Thus, the built-in Java Card protection cannot impose temporal restrictions on inter-applet communications.
In a scenario, where several independent application providers have applets on a single card, the aforementioned weakness generates a serious security risk for illicit method invocations between the interacting applets. Let us consider the typical case of a multi-applet smart card with one purse applet and two loyalty applets that are notified when card transactions occur, in order to award bonus points. Loyalty applets are communicated to by calls to methods declared in shareable interfaces. Temporal restrictions for secure applet interaction include the requirement of recursion freeness for the methods of the shareable interfaces and the absence of transitive communications that span the contexts of the two loyalty applets. In the more complex case, where a loyalty applet shares bonus points through some agreed loyalty applet to loyalty applet communication, secure interaction requires additional temporal restrictions besides those mentioned.
Apart from temporal safety, it is also important to assure that the allowed communication between the three applets does not imply unwanted information flow from one loyalty applet to the other. This is the only way to guarantee that secret and potentially commercial data produced in one applet cannot be leaked to another applet, while at the same time applets of one application cannot be crashed by other applet’s corrupt data.
Other sources of security risk are the misused Java Card API calls in combination with the multiple-entry-point program structure. Since applets run forever and their execution is suspended when the card is removed from the reader, a potentially unhandled exception that reaches the invoked entry point may leave an applet in an unpredictable state that can be dangerous for the application’s security.