ACCUEIL

Consignes aux
auteurs et coordonnateurs
Nos règles d'éthique
Auteurs : soumettez
votre article en ligne
Autres revues >>

Technique et Science Informatiques

0752-4072
Revue des sciences et technologies de l'information
 

 ARTICLE VOL 22/1 - 2003  - pp.33-60  - doi:10.3166/tsi.22.33-60
TITRE
Développement formel d'un vérifieur embarqué de byte-code Java

RÉSUMÉ
La politique de sécurité de Java est implémentée par des composants de sécurité tels que la machine virtuelle, le vérifieur ou encore le chargeur. Il est de première importance d'assurer que les implémentations de ces composants sont cohérentes vis-à-vis de leurs spécifications. Les méthodes formelles peuvent être utilisées pour apporter la preuve que les implémentations de ces composants sont conformes à leurs spécifications. Dans cet article, nous présentons le développement formel, à l'aide de la méthode B, d'un vérifieur de bytecode Java Card. Le langage complet est traité, ce qui nous fournit des métriques réalistes concernant le coût d'un développement formel. Cette formalisation se termine par l'intégration du code issu du développement dans une carte à puce.


ABSTRACT
The Java security policy is implemented by security components such as the Java Virtual Machine (JVM), the verifier and 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 this 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. This formalization leads to an embeddable implementation of the byte code verifier. We present the formal models, discuss the integration into the card and the results of such an experiment.


AUTEUR(S)
Lilian BURDY, Ludovic CASSET, Antoine REQUET

Reçu le 3 décembre 2001.    Accepté le 15 juillet 2002.

MOTS-CLÉS
algorithme de vérification, méthode B, vérifieur de byte-code, méthodes formelles, cartes à puce.

KEYWORDS
verification algorithm, B method, byte code verifier, formal methods, smart card.

LANGUE DE L'ARTICLE
Français

 PRIX
• Abonné (hors accès direct) : 12.5 €
• Non abonné : 25.0 €
|
|
--> Tous les articles sont dans un format PDF protégé par tatouage 
   
ACCÉDER A L'ARTICLE COMPLET  (359 Ko)



Mot de passe oublié ?

ABONNEZ-VOUS !

CONTACTS
Comité de
rédaction
Conditions
générales de vente

 English version >> 
Lavoisier