Using B Method to Formalize the Java Card Runtime Security Policy for a Common Criteria Evaluation
Stéphanie Motré, Corinne Téri · 1999
A smart card is an embedded system that is generally used to supply security to an information system. Traditionally the application and the OS were developed in a secure environment by the card issuer. For a few years, open platforms (e.g., Java Card, MultOS and Smart Card for Windows) have provided new facilities for application developers. They allow dynamic storage and execution of downloaded executable code. Such architecture introduces new risks: it offers the possibility to attack the card from an applet by exploiting some implementation faults. This document provides an overview of a set of techniques required to obtain Common Criteria (CC) high Evaluation Assurance Levels (EALs) of a Java Card. It is not dedicated to smart card specialists as it presents the security stakes of such a technology. We present the motivation for a Java Card evaluation: reach the same security level for the new open smart card than for traditional embedded platforms. We introduce the UML and the B method to illustrate the semi-formal and formal models required for a high level evaluation. The B method has been already used in GEMPLUS to formally model security mechanisms of the Java Card: bytecode verifier, interpreter and firewall. These case studies reveal the interest of using the B method to formalize the Java Card Virtual Machine (JCVM). In a CC evaluation the use of semi-formal and formal techniques is required to obtain the assurance of a high security level.