A Tool for Checking Secure Interaction in Java Cards

We present an approach based on a multilevel security policy and the theory of abstract interpretation for checking secure interaction between applications in Java Cards. The security policy is defined by the user, which assigns security levels to Java Card applications. Actual values are abstracted into security levels, and an abstract interpreter executes the bytecode of applications in the abstract domain. We show JCSI, a tool that implements the presented approach. JCSI can be used to check the binary code of Java Card applications before their installation on-card.