Security Verification: a Programming Language Approach
by Thomas Jensen
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.
More information on the Lande team can be found at http://www.irisa.fr/lande/.
Please contact:
Thomas Jensen - IRISA
Tel: +33 2 99 84 74 78
E-mail: Thomas.Jensen@irisa.fr
