The new generation of smartcards provides solutions for card developers that reduce the time-to-market and allow software evolution of their already deployed smartcards. The strong typing of Java enforces the language- based security, but is not sufficient. The application security relies on a proven implementation of the OS and the associated JCRE. Ensuring the correctness of this JCRE. Ensuring the correctness of this Implementation is the basis of platform level Security. This can be done through a Mathematical proof of the implemenntation.
展开▼