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 23/3 - 2004  - pp.323-357  - doi:10.3166/tsi.23.323-357
TITRE
Validation du contrôle d'accès dans des cartes à puce multi-applications

RÉSUMÉ
Le contrôle d’accès entre applettes mis en place dans Java Card est exercé par le parefeu. Ce pare-feu peut être contourné en utilisant des objets partageables. Pour vérifier que ces contournements ne donnent pas lieu à des accès non souhaitables, nous proposons une analyse statique qui calcule une approximation des flots d’objet entre les applettes. L’analyse s’applique sur un sous-ensemble de Java Card, qui inclut le pare-feu, l’invocation de méthodes virtuelles, les accès aux champs et aux variables, les objets partageables ainsi que la notion de contexte.

Elle est basée sur l’utilisation d’un nouveau type de contraintes : les contraintes conditionnelles quantifiées. Ces contraintes permettent une modélisation précise et efficace de Java Card en incluant, entre autres, les effets du pare-feu sur les exécutions. De plus, la production dynamique des contraintes est conditionnée par l’acceptation de l’accès par le pare-feu.

ABSTRACT

The access control exercised by the Java Card firewall can be bypassed by the use of shareable objects. To help detecting unwanted access to objects, we propose a static analysis that calculates a safe approximation of the possible flow of objects between Java Card applets. The analysis deals with a subset of the Java Card bytecode focussing on aspects of the Java Card firewall, method invocation, field access, variable access, shareable objects and contexts. The technical vehicle for achieving this task is a new kind of constraints: quantified conditional constraints, that permits us to model precisely yet cost-effectively the effects of the Java Card firewall by only producing a constraint if the corresponding operation is authorized by the firewall.

AUTEUR(S)
Marc ÉLUARD, Thomas JENSEN

Reçu le 25 octobre 2002.    Accepté le 16 juin 2003.

MOTS-CLÉS
sécurité, carte à puce, Java Card, analyse statique, contraintes et vérification.

KEYWORDS
security, smart card, Java Card, static analysis, constraints and verification.

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  (307 Ko)



Mot de passe oublié ?

ABONNEZ-VOUS !

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

 English version >> 
Lavoisier