BOM : Traduction du langage formel B optimisant la consommation mémoire

Résumé

Les cartes à puce sont un moyen de sécuriser un système d'information. Elles sont donc soumises à de fortes exigences en terme de sécurité. Avec l'apparition des cartes ouvertes, permettant de charger de nouvelles applications dans les cartes, l'utilisation de techniques formelles telles que la méthode B est nécessaire afin d'apporter une assurance en terme de sécurité au moins égale à celle des cartes traditionnelles.

De nombreux travaux sur l'utilisation de la méthode B pour les cartes à puces ont déjà été menées par Gemplus. Cependant, en raison des fortes contraintes liées à la carte à puce en terme de consommation mémoire, intégrer du code prouvé dans une carte à puce est actuellement impossible. L'utilisation de méthodes formelles est donc limitée à la validation et la preuve de spécification.

Le projet B-OM vise à fournir un traducteur de spécification B d'envergure industrielle permettant d'embarquer du code prouvé dans une carte à puce. Ceci passe premièrement par la mise en oeuvre d'optimisations mémoire avancées permettant de s'affranchir des contraintes techniques liées aux cartes à puce. Ensuite, pour permettre son utilisation industrielle, des techniques formelles seront utilisées afin d'apporter la preuve de correction des optimisations effectuées.


Partenaires du projet


Objectifs

Doter les objets d'intelligence logicielle est l'objectif du projet B-OM. Nous cherchons à améliorer la productivité des cycles de développement tout en améliorant la sécurité du logiciel en utilisant des techniques formelles. Nous visons les systèmes embarqués et principalement les cartes à puce et les objets intelligents.

Bien que les techniques formelles soient applicables sur l'ensemble du cycle de vie du développement, les contraintes en terme d'occupation mémoire de la carte font qu'actuellement ces techniques sont limitées à la phase de spécification. Une solution pour améliorer la productivité et augmenter la réactivité de l'entreprise consiste à apporter la preuve de la correction de l'implémentation. Ce moyen réduit la phase de test unitaire dont le coût représente actuellement près de la moitié du coût global d'un projet. Bien que l'utilisation de ces techniques augmente le coût de développement des phases amont ce coût est contre balancé par la réutilisabilité de ses spécifications et l'amélioration de la maintenabilité du produit.

Cependant, les outils génériques de traduction fournis par Steria nécessitent d'être adaptés aux contraintes fortes de la carte à puce. Actuellement le code généré ne permet pas d'être incorporé tel quel dans la carte dû à l'utilisation non optimisée de la mémoire. Il faut effectuer une translation manuelle ne permettant pas d'éliminer les tests unitaires. L'automatisation de cette optimisation manuelle permettrait des gains de productivité importants. Ceci, d'autant plus qu'une même application carte à puce peut être déclinée sur un nombre important de plates-formes, (8,16 ou 32 bits) nécessitant une adéquation du programme aux spécificités de la cible.

Mise en oeuvre et état de l'art

Le projet va s'appuyer sur l'expérience des différents partenaires :

La mise en commun de ces compétences va permettre de développer un traducteur optimisant, suivant des règles de génie logiciel et des techniques de preuve formelle permettant une éventuelle certification de ce traducteur si requise.

Ruptures technologiques

La principale difficulté technique qui sera levée lors du projet B-OM concerne la validation de la correction des optimisations effectuées par le traducteur. Bien que de nombreux travaux de recherche existent sur la preuve de correction de compilateurs, une telle validation est rarement rencontrée sur des cas d'envergure industrielle. Dans le cadre du projet B-OM, elle s'avère nécessaire afin de fournir une assurance forte de la correction des traductions effectuées par le traducteur.

Cette assurance sera apportée pour chaque type d'optimisation, par l'intermédiaire de preuve formelle à l'aide de la méthode B, de validation au méta-niveau ou de traduction systématique, en fonction des propriétés de ces optimisations.

Organisation du projet

La première étape de ce projet correspondra à la définition des techniques d'optimisation devant être incorporées au traducteur. Cette phase fera intervenir d'une part les compétences de Gemplus dans l'écriture de programme pour carte à puce, ainsi que l'expertise du LSR liée aux aspects théoriques de la méthode B.

A partir de cette définition, la réalisation du traducteur se découpera en deux tâches :

Parallèlement à ces travaux, un cas d'étude représentatif de développement B pour la carte à puce sera développé, afin de disposer d'une spécification publique permettant de quantifier les gains obtenus par l'utilisation du traducteur optimisant. La réalisation de ce cas d'étude, défini comme une machine virtuelle similaire à la machine virtuelle Java Card fera intervenir l'ensemble des partenaires.

Retombées du projet

La première retombée attendue est tout d'abord l'augmentation de la qualité et de la sûreté des cartes à puce, grâce à l'utilisation de la méthode B pour le développement.

De plus, certaines techniques d'optimisations développées lors du projet B-OM, et non spécifiques à la carte à puce pourront être utiles à d'autres contextes embarqués. La mise à disposition sous forme de logiciel libre d'une version de ce traducteur permettra une meilleure diffusion de la méthode B, aussi bien au niveau de son utilisation industrielle que de son enseignement.

Enfin, les résultats concernant la validation des optimisations ainsi que ceux concernant l'évaluation du traducteur feront l'objet de publications.