FACADE: A Typed Intermediate Language Dedicated to Smart Cards

Abstract

The use of smart cards to run software modules on demand has become a major business concern for application issuers. Such down-loadable executable content needs to be trusted by the card execution environment in order to ensure that an instruction on a memory area is compliant with the definition of the data stored in this area (i.e. its type). Current solutions for smart cards rely on three techniques. For Java Card, either an off-card verifier-converter performs a static verification of type-safety, or a defensive virtual machine performs the verification at runtime. For other types of open smart cards, no type-checking is carried out and the trust is only based on the containment of applications. Static verification is more efficient and flexible than dynamic techniques. Nevertheless, as the Java verifier cannot fit 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-safety verification can be performed statically on-card.