5th International Workshop on
Formal Methods for Industrial Critical Systems
Berlin, April 3-4, 2000
A B Model for Ensuring Soundness of a Large Subset
of the Java Card Virtual Machine
Java Cards are a new generation of smart cards that use the Java
programming language. As smart cards are usually used to supply security to a
system, security requirements are very strong and certification can become a
competitive advantage. Such a certification to a high Common Criteria or
ITSEC level requires the proof of all the security mechanisms. Those security
mechanisms include the byte code interpreter and verifier of the virtual
machine. Previous works have been done on methodology for proving the
soundness of the byte code interpreter and verifier using the B method. It
refines an abstract defensive interpreter into a byte code verifier and a byte code
interpreter. However, this work had only been tested on a very small subset of
the Java Card instruction set. This paper presents a work aiming at verifying the
scalability of this previous work. The original instruction subset of about ten
instructions has been extended to more than one hundred instructions, and the
additional cost of the proof has been managed by modifying the specification in
order to group opcodes by properties.
Note: The content of the following files is part of
GMD Report No. 91
and subject to its copyright.
ERCIM FMICS Home Page,
GMD FOKUS Home Page
Last modified: Wednesday, 19-Apr-2000 08:57:51 MET DST,
Axel Rennoch