Publication Details

Java Card is a variant of Java designed for use in smart cards and other systems with limited resources. Applets running on a smart card are protected from each other by the applet firewall, allowing communication only through shared objects. Security can be breached if a reference to a shared object is leaked to a hostile applet.

In this paper we develop a Control Flow Analysis for a small language based on Java Card, which will guarantee that sensitive object references can not be leaked to a particular (attack) applet. The analysis is used as a basis for formulating a hardest attacker that will expand the guarantee to cover all possible attackers.