La vérification de bytecode Java: le pons asinorum des analyses statiques de sécurité

Xavier Leroy

Projet Cristal INRIA Rocquencourt

21 Juin 2002, 14h30, E-006

Résumé:
La vérification de bytecode est un composant de sécurité crucial pour l'exécution sans risques d'applets Java, aussi bien dans des navigateurs Web que dans des systèmes embarqués comme les cartes à puce JavaCard. Il s'agit d'une analyse statique de code compilé qui établit au moment du chargement des propriétés de bon typage du code et d'intégrité de la machine virtuelle Java.

Bien que conceptuellement simple (c'est une analyse de type dataflow), la vérification de bytecode Java se révèle étonnamment difficile à mettre en oeuvre de manière correcte et sûre: certains traits du bytecode Java (subroutines, initialisation des objets) sont délicats à analyser, et spécifiés de manière insuffisamment précise. Ceci en fait un objet d'étude intéressant, tant pour concevoir et spécifier les algorithmes de vérification que pour les valider formellement.

Dans cet exposé, j'essaierai de donner une présentation unifiée de plusieurs techniques de vérification de bytecode, en insistant plus particulièrement sur

1. le problème des subroutines,
2. les algorithmes de vérification adaptés aux petits systèmes embarqués tels que les cartes à puces.

Retour au sommaire / Back to schedule