Security and Safety through Static Analysis

by Chris Hankin and Thomas Jensen

Static analysis of programs is a proven technology in the implementation of compilers and interpreters. Recent years have begun to see application of static analysis techniques in areas such as software validation and software re-engineering. 'Secsafe' is an IST project that aims at demonstrating that static analysis technology facilitates the validation of security and safety aspects of systems based on the Internet and on smart cards.

With its use of programmable smart cards and payment via the Internet, electronic commerce must guarantee the confidentiality and integrity of the data involved in transactions. The ever-increasing presence of software in these applications means that verifying that this software conforms to such security requirements becomes an all-important task which is far from trivial. The IST project'Secsafe' has as its aim the development of methods for validating the safety and security of software that apply to both domains. This has led to the project focussing a substantial part of its efforts on the Java programming language and its dialect Java Card, dealing with both source-level and bytecode-level applications. The project is divided into five activities: specification of security properties, semantics, static analysis, algorithms and tools. The partners in the project are Imperial College (coordinator), the Technical University of Denmark, INRIA and the SME Trusted Logic SA.

The primary thrust of the project has been the security of multi-application smart cards programmed using the Java Card language. Results so far include a list of security properties that Java Card applets should satisfy. Among other things, these properties are concerned with the allocation of memory, the handling of exceptions and the flow of information between applets. Another tangible outcome of the project is the definition of the Carmel intermediate language and its semantics. The Carmel language is distilled from the Java Card bytecode language with the aim of providing a small set of bytecodes that retains all the features of Java Card. This language has been given an operational semantics that specifies in detail the action of each Carmel instruction. In particular, it describes the workings of the firewall that separates the applets installed on a multi-application Java Card.

The verification of security properties is done by a static analysis that will build a correct approximation of the dynamic behaviour of the applets. This approximation will include a description of how data and objects flow between applets, which methods are called by a given applet and which instructions might lead to a security exception being raised. The project aims at developing a family of analyses such that the precision and cost of an analysis can be adjusted to the verification problem at hand. The flow logic framework for specifying static analyses has been chosen as an appropriate technology for ensuring this flexibility. It will be combined with powerful constraint resolution techniques in order to implement the analyses in an efficient manner.

One of the major problems in the field of multi-application smart cards is how to download applets dynamically on a card in a secure fashion. Due to the limited resources on the card, only a certain amount of verification can be done on-card. The Secsafe project contributes to overcoming this difficulty by investigating how analyses can be done as cost-effectively as possible and in a modular fashion. A first and important step towards this goal was achieved when Trusted Logic managed to design a bytecode verifier for Java Card that is efficient enough (in particular memory-wise) to be executed on-card. For this achievement, Trusted Logic won the 2001 European IST Prize. Extending this approach to other kinds of security verifications requires the development of techniques for modelling and analysing fragments of code that will support the inference of secure interfaces for applets. These interfaces will list the properties that a foreign applet must satisfy in order to ensure that its loading will not jeopardise the overall security of the card. The theoretical tools employed in this task include modular abstract interpretation and novel approaches to semantics of open systems.

Please contact:
Thomas Jensen, IRISA/CNRS, France
Tel: +33 2 99 84 74 78
E-mail: Thomas.Jensen@inria.fr