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.
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.
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.
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.
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.
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.