Résumé:
Les cartes à puce sont maintenant des mini-micro-ordinateurs
programmables avec des langages objets. Leurs capacités de calcul et de
stockage leur permettent de contenir plusieures applications. D'autre
part, les besoins de sécurité dans les systèmes d'information sont de
plus en plus importants. Aussi, nous avons besoin de méthodes pour
prouver que la sécurité attendue est bien présente dans les cartes.
Ces méthodes doivent pouvoir vérifier que les règles définissant la
sécurité protègent effectivement les données. Ces règles sont exprimées
sous forme de propriétés. Ces méthodes doivent aussi pouvoir être
utilisés dans le cadre de la certification de programmes pour valider la
mise en oeuvre des mécanismes de sécurité. Dans cette thèse, nous
donnons un ensemble de méthodes permettant de répondre à ces attentes.
Nous appliquons des techniques d'analyse statique de programme objet au
langage Java Card afin de vérifier des propriétés sur les exécutions des
programmes.
Pour offrir un degré de confiance élevé dans la certification, notre travail repose sur des bases formelles. Nous proposons ainsi une abstraction de Java Card et sa sémantique. Nous utilisons ensuite une analyse statique pour calculer un graphe de flot de contrôle en résolvant un système de contraintes. Pour affiner les résultats de cette analyse, nous utilisons un nouveau type de contraintes : les contraintes conditionnelles quantifiées. Nous fournissons la preuve de correction de l'analyse ainsi que celle de validité de la recherche de point fixe. L'expression des propriétés de sécurité repose sur le formalisme des automates finis. Pour la vérification, nous comparons le langage reconnu par le graphe avec celui reconnu par l'automate afin de déterminer si les programmes respectent ces propriétés. Nous terminons en présentant des propriétés qu'il est ainsi possible d'exprimer et de vérifier.
Retour au sommaire / Back to schedule