A Type System for Checking Applet Isolation in Java Card

In: Formal Techniques for Java Programs. 2001

Authors

• Peter Müller
• Arnd Poetzsch-Heffter

Abstract

A Java Card applet is, in general, not allowed to access fields and methods of other applets on the same smart card. This applet isolation property is enforced by dynamic checks in the Java Card Virtual Machine. This paper describes a refined type for Java Card that enables mostly static checking of applet isolation. With this type system, most firewall violations are detected at compile time.

Full Text

• PDF: firewall.pdf
• PS.GZ: firewall.ps.gz

BibTeX

@InProceedings{Mueller.Poetzsch-Heffter01typesystem, 
   author = {Peter Müller and Arnd Poetzsch-Heffter}
   title = {A Type System for Checking Applet Isolation in Java Card},
   booktitle = {Formal Techniques for Java Programs},
   year = {2001},
}