Formal development of an embedded verifier for Java Card byte code

The Java security policy is implemented by security components such as the Java Virtual Machine (JVM), the API, the verifier, the loader. It is of prime importance to ensure that the implementation of these components is in accordance with their specifications. Formal methods can be used to bring th...

Full description

Saved in:
Bibliographic Details
Main Authors: Casset, L., Burdy, L., Requet, A.
Format: Conference Proceeding
Language:English
Subjects:
Applied sciences
Automata. Abstract machines. Turing machines
Computer science
control theory
systems
Data security
Error correction codes
Exact sciences and technology
Information systems
Java
Protection
Prototypes
Smart cards
Theoretical computing
Virtual machining
Online Access:Request full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:The Java security policy is implemented by security components such as the Java Virtual Machine (JVM), the API, the verifier, the loader. It is of prime importance to ensure that the implementation of these components is in accordance with their specifications. Formal methods can be used to bring the mathematical proof that the implementation of these components corresponds to their specification. In the paper, a formal development is performed on the Java Card byte code verifier using the B method. The whole Java Card language is taken into account in order to provide realistic metrics on formal development. The architecture and the tricky points of the development are presented. This formalization leads to an embeddable implementation of the byte code verifier thanks to automatic code translation from formal implementation into C code. We present the formal models, discuss the integration into the card and the results of such an experiment.
DOI:10.1109/DSN.2002.1028886