Are Smart Cards the Ideal Domain for Applying Formal Methods

Abstract

The traditional approach for programming smart cards does not allow the creation of downloadable executable code and requires programmers with experience in programming in low-level languages. This approach, associated with a high quality qualification process, produce secured smart card. Unfortunately, it does not allow card manufacturers and issuers to quickly respond to the market changes, and it limits the flexibility of smart card applications. Open smart card programming provides a more dynamic approach to card applications. High-level languages and security mechanisms are the basis for the programming of open smart cards. Most notable efforts towards such smart card systems are Java Card [22], MultOS [14] and Smart Card for Windows [15], which provide application developers an opportunity to develop rapidly applications. The main drawback with this kind of smart card is the risk to download a hostile application that will exploit a faulty implementation module of the platform. Security is always a big concern for smart cards, but the issue is getting more intense with multi-applicative platforms and post issuance code downloading. The correct design and implementation of the system is the key to shun such an attack. Fault prevention offers different techniques to remove latent errors from the system. The fault avoidance concerns methodologies and appropriate techniques to avoid the introduction of fault during the design and the construction of the system. In a first approach, one can believe that smart card can only get benefits of using formal methods.