JCSI: A tool for checking secure information flow in Java Card applications

This paper describes a tool for checking secure information flow in Java Card applications. The tool performs a static analysis of Java Card CAP files and includes a CAP viewer. The analysis is based on the theory of abstract interpretation and on a multi-level security policy assignment. Actual values of variables are abstracted into security levels, and bytecode instructions are executed over an abstract domain. The tool can be used for discovering security issues due to explicit or implicit information flows and for checking security properties of Java Card applications downloaded from untrusted sources.

► We use a multilevel security policy to define the allowed information flow between packages.
► We define a full set of abstract rules for bytecode to trace information flow.
► We design an abstract interpreter that reduces the complexity of the analysis using a dataflow fixpoint iteration.
► The implemented tool performs a modular analysis of packages; no annotation of code is required.
► The tool is downloadable from www.eecs.qmul.ac.uk/~masci/JCSI.