-1 color=black>

Trading-O Type-Inference Memory Complexity Against Communication
Trading-O Type-Inference Memory Complexity
Against Communication
Konstantin Hypp�onen
1
, David Naccache
2
, Elena Trichina
1
, and Alexei
Tchoulkine
2
1
University of Kuopio
Department of Computer Science
Po.B. 1627, FIN-70211, Kuopio, Finland
{konstantin.hypponen, elena.trichina}@cs.uku.fi
2
Gemplus Card International
Applied Research & Security Centre
34 rue Guynemer, Issy-les-Moulineaux, 92447, France
{david.naccache, alexei.tchoulkine}@gemplus.com
Abstract. While bringing considerable exibility and extending the
horizons of mobile computing, mobile code raises major security issues.
Hence, mobile code, such as Java applets, needs to be analyzed before ex-
ecution. The byte-code verier checks low-level security properties that
ensure that the downloaded code cannot bypass the virtual machines se-
curity mechanisms. One of the statically ensured properties is type safety.
The type-inference phase is the overwhelming resource-consuming part
of the verication process.
This paper addresses the RAM bottleneck met while verifying mobile
code in memory-constrained environments such as smart-cards. We pro-
pose to modify classic type-inference in a way that signicantly reduces
the memory consumption in the memory-constrained device at the detri-
ment of its distrusted memory-rich environment.
The outline of our idea is the following, throughout execution, the mem-
ory frames used by the verier are MAC-ed and exported to the terminal
and then retrieved upon request. Hence a distrusted memory-rich ter-
minal can be safely used for convincing the embedded device that the
downloaded code is secure.
The proposed protocol was implemented on JCOP20 and JCOP30 Java
cards using IBMs JCOP development tool.
1
Introduction
The Java Card architecture for smart cards [1] allows new applications, called
applets, to be downloaded into smart cards. While general security issues raised
by applet download are well known [9], transferring Javas safety model into
resource-constrained devices such as smart cards appears to require the devising
of delicate security-performance trade-os.
When a Java class comes from a distrusted source, there are two basic man-
ners to ensure that no harm will be done by running it. The rst is to interpret the code defensively [2]. A defensive interpreter is
a virtual machine with built-in dynamic runtime verication capabilities. De-
fensive interpreters have the advantage of being able to run standard class les
resulting from any Java compilation chain but appear to be slow: the security
tests performed during interpretation slow-down each and every execution of
the downloaded code. This renders defensive interpreters unattractive for smart
cards where resources are severely constrained and where, in general, applets are
downloaded rarely and run frequently.
Another method consists in running the newly downloaded code in a com-
pletely protected environment (sandbox), thereby ensuring that even hostile code
will remain harmless. In this model, applets are not compiled to machine lan-
guage, but rather to a virtual-machine assembly-language called byte-code.
Upon download, the applets byte-code is subject to a static analysis called
byte-code verication which purpose is to make sure that the applets code is
well-typed. This is necessary to ascertain that the code will not attempt to violate
Javas security policy by performing ill-typed operations at runtime (e.g. forging
object references from integers or calling directly API private methods). Todays
de facto verication standard is Suns algorithm [7] which has the advantage
of being able to verify any class le resulting from any standard compilation
chain. While the time and space complexities of Suns algorithm suit personal
computers, the memory complexity of this algorithm appears prohibitive for
smart cards, where RAM is a signicant cost-factor.
This limitation gave birth to a number of innovating workarounds:
Leroy [5, 6] devised a verication scheme which memory complexity equals the
amount of RAM necessary to run the veried applet. Leroys solution relies on
o-card code transformations whose purpose is to facilitate on-card verication
by eliminating the memory-consuming x-point calculations of Suns original
algorithm.
Proof carrying code [11] (PCC) is a technique by which a side product of
the full verication, namely, the nal type information inferred at the end of
the verication process (x-point), is sent along with the byte-code to allow a
straight-line verication of the applet. This extra information causes some trans-
mission overhead, but the memory needed to verify a code becomes essentially
equal to the RAM necessary to run it. A PCC o-card proof-generator is a rather
complex software.
Various other ad-hoc memory-optimization techniques exist as well [10, 8].
Our results: The work reported in this paper describes an alternative byte-
code verication solution. Denoting by M
max
the number of variables claimed
by the veried method and by J the number of jump targets in it, we show
how to securely distribute the verication procedure between the card and the
terminal so as to reduce the cards memory requirements from O(M
max
J) to
O(J log J + cM
max
) where c is a small language-dependent constant or, when a
higher communication burden is tolerable, to a theoretic O(log J + cM
max
).
The rest of the paper is organized as follows: the next section recalls Javas
security model and Suns verication algorithm with a specic focus on its data- ow analysis part. The subsequent sections describe the new verication proto-
col, which implementation details are given in the last section.
2
Java Security
The Java Virtual Machine (JVM) Specication [7] denes the executable le
structure, called the class le format, to which all Java programs are compiled.
In a class le, the executable code of methods (Java methods are the equivalent
of C functions) is found in code-array structures. The executable code and some
method-specic runtime information (namely, the maximal operand stack size
S
max
and the number of local variables L
max
claimed by the method
3
) constitute
a code-attribute. We briey overview the general stages that a Java code goes
through upon download.
To begin with, the classes of a Java program are translated into independent
class les at compile-time. Upon a load request, a class le is transferred over
the network to its recipient where, at link-time, symbolic references are resolved.
Finally, upon method invocation, the relevant method code is interpreted (run)
by the JVM.
Javas security model is enforced by the class loader restricting what can be
loaded, the class le verier guaranteeing the safety of the loaded code and the
security manager and access controller restricting library methods calls so as
to comply with the security policy. Class loading and security management are
essentially an association of lookup tables and digital signatures and hence do not
pose particular implementation problems. Byte-code verication, on which we
focus this paper, aims at predicting the runtime behavior of a method precisely
enough to guarantee its safety without actually having to run it.
2.1
Byte-Code Verication
Byte-code verication [4] is a link-time phase where the methods run-time be-
havior is proved to be semantically correct.
The byte-code is the executable sequence of bytes of the code-array of a
methods code-attribute. The byte-code verier processes units of method-code
stored as class le attributes. An initial byte-code verication pass breaks the
byte sequence into successive instructions, recording the oset (program point)
of each instruction. Some static constraints are checked to ensure that the byte-
code sequence can be interpreted as a valid sequence of instructions taking the
right number of arguments. As this ends normally, the receiver assumes that the
analyzed le complies with the general syntactical description of the class le
format.
Then, a second verication step ascertains that the code will only manipulate
values which types are compatible with Javas safety rules. This is achieved by a
type-based data-ow analysis which abstractly executes the methods byte-code,
3
M
max
= L
max
+ S
max
. by modelling the eect of the successive byte-codes on the types of the variables
read or written by the code.
The next section explains the semantics of type checking, i.e., the process
of verifying that a