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.
For more information, see [BartheDJSS01] and [BartheDJS02], or contact Gilles Barthe.
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 machine.
JSL specifications can be translated into SPIKE specifications, and into Coq and PVS specifications (via an intermediate format with case-expressions).
For more information, see [BartheDHS01], [BartheC02], and [BartheCDS02], or contact Gilles Barthe.
Outcome of the project so-far is a framework containing:
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
For more information, see [BartheGH01], [BartheGH02], and the deliverable Description of JCTLS & Toolset for applet verification, or contact Marieke Huisman.
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 [CatanoH02], [TrentelmanH02], and the deliverable Description of JCISL, or contact Marieke Huisman.
Last modified: Fri Sep 19 17:12:13 MEST 2003