Firstly, new smart cards applications (such as loyalty) are characterized by the gathering of several partners who bring each one their application part in order to offer a global service to the mobile user. These applications implies new requirements in embedded software lifecycle. It is indeed necessary that each partner have to be able to make evolve his part without breaking the whole application. Moreover, it is necessary to allow the evolution of the cooperation scheme (like modification of resource sharing or the arrival of new partners). Secondly, the use of smart cards to run software modules on demand becomes a major business concern for application issuers. Such downloadable 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.
This presentation addresses these previous aspects. We firstly present the Hybrid smart card project, which aims to increase the cooperation facility in multi-partner smart card applications. The current models of smart cards, databases or multi-applications cards, can not take fully into account the new needs previously enounced (i.e. secure and flexible resource sharing and flexible evolution). We intend to show that their coupling however makes it reach that goal. After a glance at these two main models, we will present the Hybrid smart card, which can be seen as a fusion of both. Secondly, we present the FACADE project, which proposes a static type-safety on-card verification. After an overview of code safety techniques, we will present the FACADE solution. The FACADE language is defined as a target language for on-card application execution. This language is quite simple and aims to ease static inside verification. We will focus on the verification process.