FACADE: A Typed Intermediate Language Dedicated to Smart Cards

The use of smart cards to run software modules on demand has become a major business concern for application issuers. Such downloadable executable content requires to be trusted by the card execution environment in order to ensure that an instruction on a memory area is compliant with the de nition of the data stored in this area i.e. its type. Current solutions for smart cards rely on three techniques: for Java Card, 1 an o -card veri er-converter performs a static veri cation of type-safety, or 2 a defensive virtual machine performs the veri cation at runtime; for others, 3 no type-checking is carried out and the trust is only based on the containment of applications. Static veri cation is more e cient and exible than dynamic techniques. Nevertheless, as the Java veri er cannot t into a card, the trust is dependent on an external third-party. In this way, the card security has been partly turned to the outside. We propose and describe the FACADE language for which the type-sa...

• Type: Conference
• Year: 1999
• Where: ESEC
• Authors: Gilles Grimaud, Jean-Louis Lanet, Jean-Jacques Vandewalle
• Keywords: ESEC 1999, Software Engineering, Static Veri Cation, Type-safety Veri Cation, Veri Cation