Programming Language Approdcues

Electronic commerce with its use of programmable smart cards and payment via Internet must guarantee the confidentiality and integrity of the data involved in the 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 Lande research team at IRISA (Inria-Rennes) studies formal techniques for verifying security properties of applications written in the Java programming language and its dialect Java Card, destined for smart card programming.

A number of programming languages incorporate facilities for rendering a program secure eg, by protecting data from unwanted access or by limiting the capabilities of parts of code whose behaviour cannot be trusted. Using a high-level language to express the security management in a program (as opposed to relying on low-level or hardware mechanisms) facilitates formal reasoning about its correctness and opens up the possibility of using well-established techniques from programming language semantics to structure this reasoning. A recent example is Java that comes equipped with a complex security architecture which includes visibility modifiers to limit the accessibility of members of classes, the use of class loaders to create separate name spaces, granting of user-defined permissions such as reading and writing files, and dynamic checks that the executing code has a given permission.

The aim of our research is to develop methods that allow to verify security claims of such applications in a formal manner. This involves two activities: the formalisation of what a security claim is and a semantic model of the Java security architecture against which these security claims can be checked. Our initial effort has focussed on control-flow-based security that for a given code traces back in the execution history to discover on whose behalf it is executing, in order to check that those who originated the current operation indeed have the right to do so. Prior to verification, a program is submitted to a type analysis that for each (virtual) method invocation in the program returns an approximation of the set of concrete methods to which this invocation can correspond - this results in an approximate control flow graph for the program. From this graph we derive a transition system where the states are call stacks and where transitions are method invocations. The security properties to verify are formalised using a temporal logic that describes the allowed paths that can be taken in this transition system. The transition system is infinite and we rely on a novel reduction technique that for a given property allows to restrict attention to a finite part of the transition system in order to verify the validity of the property. The actual verification then becomes a classical model-checking problem.

Ongoing research in the group aims at extending these results in two directions. First, the current method requires that all of the program to verify must be present. This is a limitation in a world where code is loaded dynamically over networks. In order to solve this problem we are looking at how to modularise the various static analyses involved. The aim is a technique that for each unknown piece of code derives a security interface, ie, a security property that an imported piece of code must satisfy in order to be loaded. Second, we are in the process of applying this technique to the Java Card language for programming smart cards. Java Card is derived from Java by removing a number of language features that are too costly and not strictly necessary to implement on the resource-limited smart cards (no multi-threading, no floating-point values, no dynamic class loading etc.). The security model is somewhat different in that applications are completely isolated and communicate via explicitly shared objects. This activity is conducted in collaboration with Bull via the GIE Dyade between INRIA and Bull, and in the INRIA-sponsored research action Java Card, co-ordinated by the Lande research team.