For more information on the research done within VerifiCard at INRIA,
see also the full list of
CertiCartes is a formalisation of the JavaCard platform in Coq.
It contains formal specifications of:
All specifications are written in an executable style and model
one-step execution of the virtual machines.
- a defensive JavaCard virtual machine, i.e. a virtual machine
where values are tagged by their type and where typing information is
verified at run-time;
- an offensive JavaCard virtual machine,
i.e. a virtual machine which relies on successful bytecode
verification to eliminate type verification at run-time and where
values are untyped;
- an abstract JavaCard virtual machine, i.e. a virtual machine
whose values are only types, and which is used in the construction of the
Further, CertiCartes contains the specification of the bytecode
verifier as a data-flow analyzer based on the abstract virtual
machine; currently the bytecode verifier does not deal with object
initialization. Finally, CertiCartes establishes the correctness of
our bytecode verifier by showing that the offensive and defensive virtual
machines coincide on those programs that pass bytecode verification.
The proof relies on showing that the abstract virtual machine is a
sound abstraction of the defensive virtual machine, and that the
offensive abstract virtual machine is a sound abstraction
of the defensive virtual machine.
Both formalisations and proofs have been carried out in the proof
assistant Coq. The formal
descriptions of the virtual machines are available here.
or contact Gilles Barthe.
Jakarta is a toolset for specifying and
reasoning about the JavaCard platform. The main ingredients of the
Goal of the work is to derive certified Byte Code Verifiers by
abstraction from the specification of the JavaCard Virtual Machine.
- the Jakarta Specification Language (JSL), a front-end for producing
highly readable executable specifications;
- the Jakarta Transformation Kit (JTK), a program to manipulate and
transform JSL specifications by abstraction and refinement;
- the Jakarta Prover Interface (JPI), a compiler that translates JSL
specifications into proof assistants;
- the Jakarta Automation Kit (JAK), a toolset to support reasoning
about executable specifications within proof assistants.
The tool takes the JavaCard Virtual Machine specification
that is developed in Coq - in the context of the CertiCartes project - as
input. This is a defensive virtual machine, and by abstraction it can
be transformed into a byte code verifier plus an offensive virtual
JSL specifications can be translated into SPIKE specifications, and
into Coq and PVS specifications (via an intermediate format with
For more information, see
contact Gilles Barthe.
- Compositional specification and verification techniques
Typical for the new-generation multi-application smart cards is that
applets can be loaded post-issuance, i.e. after
initialisation of the card. In this project we look at compositional
verification of smart card programs, stating which properties should
be satisfied by the components of the system, to ensure the global
correctness of the system. When issuing a new applet on the card, one
has to check that this new applet satisfies these required properties,
in order to know that other applets can safely cooperate with it.
Outcome of the project so-far is a framework containing:
- a program model for multi-application programs;
- a specification language to express security properties of the
global system and the components;
- a proof system to show the correctness of the decomposition, which
has been proven sound w.r.t. the program model.
This work is done in close collaboration with the VerifiCard partners
at SICS (and KTH). At SICS, the
Erlang Verification Tool (EVT) is adapted for our proof system, a
first version is available as the VeriCode Proof Tool
(VCPT). Also at SICS, a toolset has been built for model checking
JavaCard applets on the bytecode level. The toolset JavaCard Applet
Verification Environment (JCAVE) is available.
Current work focuses on
- establishing a structural property language, which allows checking
properties based on the control graph of a program only,
and which will imply properties expresssed in the general
- investigating completeness of (fragments of) the proof system is
For more information, see [BartheGH01], [BartheGH02], and the deliverable Description
of JCTLS & Toolset for applet verification, or contact Marieke Huisman.
- Specifications for JavaCard programs
To verify JavaCard
programs, one first has to specify their intended
behaviour. Therefore, it is important that the specification language
that is used is expressive enough. Also, it is useful if one can do
quickly an approximate correctness check on the specification, that
can find the most common mistakes. This can be done by using for
example the static checker
this project, we investigate appropriate specification
languages and appropriate specification checking techniques.
We investigate the use of ESC/Java, by specifying Gemplus's Applet
Benchmark Kit, containing the complete source code for a purse
applet. We annotate the code with specifications (pre-post
conditions, class invariants etc., and check the annotations
with ESC/Java. While specifying, we found several bugs in the
original source code. The corresponding ESC/Java
annotations are available here.
ESC/Java does not check the assignable clauses (or frame condition, or
modifiable clause) of a method specification, which states which
variables may be modified by a method. Therefore, we develop a checker
for such assignable clauses, called ChAsE.
Based on a syntactical analysis of the program, for each statement it
is checked that it does not violate the assignable clause, and a
warning is issued if this might be the case. ChAsE is not sound or
complete, but it designed to be efficient and to find the most common
specification errors. ChAsE can be downloaded.
ChAse works on JML
specifications, which are more general than ESC/Java specifications.
To increase the expressiveness of the specification language we use,
we propose an extension of JML with temporal logic
specifications. This allows to specify how objects interact. Part of
the extension is only syntactic sugar and can be translated back into
``standard'' JML, but part also allows to express properties which
were not expressable in JML before.
Current work is on defining a semantics and appropriate verification
techniques for this extension.
For more information, see
Description of JCISL,