Static Detection of Java Card Security Exceptions

Daniel Perovich

Instituto de Computación - Universidad de la República - Uruguay

8 Mars 2002, 14h30, E-003

Résumé:
Java Card is a multi-application environment. Applets from different vendors can coexists in a single card and additional applets can be downloaded after card manufacture.

An applet often stores highly sensitive information, such as electronic money, fingerprints, private criptographic keys, etc. Sharing such sensitive data among applets must be carefully limited.

In the Java Card platform applet isolation is achieved through the applet Firewall mechanism. It confies an applet to its own designated area. To fullfill this property, the JCVM performs dynamic checks whenever an object is accessed. It mantains for each object the applet which owns it. When an object is accessed, the current context is checked with the context of the applet which owns the object. If this access violate applet isolation, a Security Excetion is thrown.

Checking applet isolation dynamically is unsatisfactory as it leads to significant runtime overhead and accidental attempts to violate the Firewall are detected at runtime, that is, after the card with the defective applet has been issued, which could lead to enormous costs.

We propose a calculus for detecting statically this kind of exceptions. Based on a lattice of security levels and on annotations of the source code, illegal access acording to the Firewall protection is detected at compile time.

Retour au sommaire / Back to schedule


Nicolas Magaud
Last modified: Mon Jan 21 12:51:54 MET 2002