Over the last decade, research on
mobile code has been a hot topic and intensive
efforts have been made to reduce the risk of malicious (Java) applets
performing
a security attack. For this, a crucial functionality of the Java
Platform is the
bytecode verifier which performs a static type analysis on programs.
This kind
of analysis ensures integrity properties of the execution environment
such as
the absence of memory faults. Consequently, there has been considerable
interest
in specifying formally the Java Virtual Machine and proving the
correctness of
its bytecode verifier (see for instance [
3,
2,
7,
6,
8) .
More recently, these investigations have been extended to establishing
an
additional property that contributes to
guarantee the
safety of bytecode by
ensuring
bounds on the computational resources needed by its execution.
Within this context, a project has been undertaken [
1]
which focuses on a rather
standard first-order functional programming language with inductive
types,
pattern matching, and call-by-value, to be executed on a simple
stack machine.
The language comes with various bytecode static analyses:
a standard type analysis,
an analysis on
the algebraic shape of the values in the stack, an analysis of
the
size of these
values, and an analysis that insures the termination. The last
three
analyses, and in particular their combination, are instrumental in
predicting the
space and time required for the execution of a program.
Here are the formal specification of the virtual machine related to
this language
and the certification in the Coq proof assistant of
an extended bytecode verifier
which performs the first two phases
of the analysis, that is the type and shape
verifications. Our
contribution is threefold:
-
First, we design a
verifier in a uniform way, so
as both verification processes
become special cases of a general framework for data flow
analysis based on the
well known algorithm due to Kildall [
5].
-
Second, we propose a
functional specification in Coq of Kildall's algorithm and
we prove its
correctness. This is related to Klein and Nipkow's work
with the
system Isabelle/HOL [
7,
6]. However
our formalization differs from theirs by theheavy
use of Coq dependent types and the way of encoding a recursive function
which is not
structurally recursive. With this approach, properties common to both
analyses
are established once and for all. Note that this approach also suits
size analysis,
although this remains work to be done in future.
-
Third,
these generic properties are used, for proving not only the
correctness
of
type
verification which
is now quite standard, (see [
4,
7,
8]),
but also, and
this is the novelty, that of
algebraic
shape verification.
See the
paper
for a detailed description. The structure of the
Coq development is made
explicit in a
readme file.