Une démarche pionnière pour la vérification de code binaire

Les techniques de vérification automatique de programmes reposant sur une analyse du logiciel à vérifier se basent généralement sur le code source du programme (ex : outils Frama-C et PathCrawler du LIST) ou sur un modèle du programme (ex : outils GaTEL et Ag@tha du LIST). Aucune technique actuelle de vérification sémantique automatique n’utilise le produit final, c'est à dire le code binaire seul. En effet, l'analyse de codes binaires présente davantage de difficultés que l'analyse de formalismes de plus haut niveau d'abstraction, car elle pose des problèmes très spécifiques tels que l'absence totale d'information a priori sur la structure du programme ou la prise en compte de mécanismes de très bas niveau pour la gestion du contrôle (exceptions, sauts calculés, manipulation de la pile…) ; il est donc naturel de s’appuyer de préférence sur un formalisme de haut niveau.
Il existe cependant un besoin industriel fort pour des analyses de sûreté ou de sécurité basées sur le seul code binaire du logiciel. Ces techniques sont notamment indispensables pour comprendre l’origine des attaques informatiques (virus, chevaux de Troie), détecter des vulnérabilités introduites par la compilation ou par une optimisation (failles du compilateur, ordre d’évaluation…), la certification de composants logiciels achetés « sur étagère » (dont on ne possède pas le code source) ou pour la vérification de programmes écrits (totalement ou partiellement) en assembleur ou dans un langage pour lequel aucun analyseur moderne n'est disponible (Pascal, Fortran, Cobol, ADA…).
Pour répondre au besoin exprimé par EDF de certification de composants achetés « sur étagère », le LIST a récemment développé une technique novatrice de vérification de code binaire. Dérivé des techniques de génération de tests pour langage C déjà mises en œuvre au LIST, l'outil OSMOSE permet de reconstruire automatiquement un modèle de la structure de contrôle du programme original et de générer des tests couvrant le code binaire. L’un des principaux atouts d’OSMOSE est sa généricité vis-à-vis du jeu d’instruction sur lequel repose le code analysé : le code est traduit (par un module ad hoc) en une représentation interne à OSMOSE et l’analyse est ensuite faite sur cette représentation. Seul le module de traduction doit être développé pour qu’OSMOSE prenne en compte un nouveau jeu d’instructions.
Suite au développement réussi de l’outil Osmose, la reconnaissance de la qualité des recherches du LIST s’est traduite par deux publications IEEE† ; EDF souhaite utiliser OSMOSE dès 2010 pour renforcer le dossier de sûreté de programmes écrits initialement en assembleur 6800, actuellement en activité mais nécessitant des rénovations partielles (dans le cadre de la troisième visite décennale des centrales nucléaires 1300MW).
La démarche du LIST s’est avérée pionnière, y compris au niveau mondial, pour la vérification de sûreté à partir du seul code binaire. Le projet ANR BINCOA (2009-2012), coordonné par le LIST, sera l'occasion de créer et fédérer une communauté d'académiques et d'industriels intéressés cette thématique : l’objectif est d'atteindre rapidement une taille critique et la reconnaissance mondiale. Les compagnies Trusted Labs (audit sécuritaire de cartes à puce) et Hispano-Suiza (équipementier aéronautique) ont déjà fait part de leur intérêt pour OSMOSE et rejoint le projet BINCOA.