Projet GECCOO - Résumé

L'objectif du projet est de proposer des méthodes et des outils pour le développement de programmes orientés objets offrant des garanties fortes de sécurité. Le projet s'intéresse plus spécifiquement à des programmes embarqués sur des cartes à puce ou dans des terminaux qui sont décrits dans des sous-ensembles de Java (par exemple JavaCard). Les travaux récents ont montré l'intérêt de spécifier des programmes Java à l'aide de formules exprimées dans le langage JML et la possibilité de construire des outils de vérification qui transforment un programme annoté en un ensemble d'obligations de preuve qu'il faut ensuite démontrer.

Cependant les premières expériences menées ont permis d'identifier plusieurs verrous que ce projet se propose d'attaquer. Tout d'abord, les contraintes de correction et de sécurité des applications doivent être exprimées dès la phase de conception du système. Il convient de les spécifier dans un langage de haut niveau, le système étant ensuite raffiné jusqu'à des programmes exécutables et efficaces. Les étapes de raffinement peuvent nécessiter la résolution d'obligations de preuves. Les obligations de preuves engendrées pour la correction de programmes objets nécessitent de raisonner sur les états de la mémoire, ces preuves sont laborieuses mais assez spécifiques, il est nécessaire de développer des procédures automatiques de preuves adaptées à ces cas. Enfin il est rare qu'une spécification et un programme soient corrects du premier coup. Le système doit donc détecter le plus tôt possible les erreurs et permettre d'utiliser les obligations de preuve pour engendrer des tests ou produire un code défensif dans le cas où certaines propriétés ne peuvent être garanties de manière statique.

Les méthodes développées dans ce projet auront un champ large d'application dans les environnements destinés à produire du code objet garanti correct par rapport à des spécifications formelles. Une attention particulière sera apportée à mettre en {\oe}uvre ces techniques dans les outils développés par les partenaires du projet.

Le projet met en relation des équipes dont l'expertise est diversifiée (preuves automatiques, générateur d'obligations de preuves, modèles objets, raffinement, sécurité des applications JavaCard, génération de tests). En effet, la réussite de la chaîne de développement que nous voulons mettre en place dépend fortement de la bonne articulation des différents maillons.