Techniques symboliques pour l'analyse de code binaire – BINCOA

L'analyse de programmes au niveau du code binaire et non du langage source est une problématique peu abordée jusqu'ici par la communauté académique mais pour laquelle l'intérêt scientifique et les besoins industriels commencent à émerger, aussi bien en sûreté de fonctionnement qu'en sécurité. On peut citer comme applications possibles : en sécurité, l'analyse de virus ou la détection de vulnérabilités typiques comme les débordements de la pile d'appel , en sûreté, la vérification de composants génériques achetés sur étagère, la vérification de correction de code optimisé, la vérification de code source contenant des portions d'assembleur, etc. Ce type de programme pose cependant des problèmes originaux non résolus dans l'état de l'art, par exemple : l'absence de flot de contrôle à priori, le flot de contrôle non structuré et la sémantique bas niveau des instructions. Le CEA LIST a développé des compétences de pointe dans ce domaine (prototype OSMOSE), mais ne peut à lui seul développer un outil et l'état de l'art. Le présent projet, en mettant en collaboration des équipes académiques de haut niveau intéressées par le sujet et des industriels concernés par la thématique, se propose de faire progresser l'état de l'art sur le domaine et de développer en France une communauté pionnière dans un domaine de recherche novateur aux applications industrielles à moyen terme. Nous nous situons dans un cadre de détection de défauts et de génération de tests plutôt que de vérification formelle au sens strict. En contre-partie, nous voulons rester au plus près du problème réel en évitant des hypothèses de modélisation trop fortes, afin d'assurer que les techniques développées pourront réellement être appliquées sur des programmes industriels. Nous envisageons d'attaquer le problème avec des combinaisons originales de concepts issus de différentes communautés : calcul symbolique des états (model checking), exécution symbolique de chemin (génération de tests) et exécution dynamique (simulation). Une partie des résultats sera implantée, soit dans OSMOSE directement soit dans des prototypes autonomes. Dans ce cas des passerelles de et vers OSMOSE seront mises en oeuvre. Les partenaires industriels joueront un rôle important, pour aider à spécifier les besoins, assurer l'adéquation des modèles retenus aux problèmes réels, fournir des études de cas réalistes, évaluer l'apport des méthodes développées et proposer des méthodologies d'utilisation. Notre partenariat bénéficie d'atouts forts pour mener à bien ces objectifs ambitieux. Les partenaires académiques sont internationalement reconnus pour leurs fortes compétences dans les techniques symboliques et possèdent tous une solide expérience en développement de prototypes, études de cas et coopérations industrielles. Les partenaires industriels viennent de différents métiers (énergie, aéronautique, sécurité) ce qui assure une vision large des besoins en analyse de code binaire. Enfin, le projet pourra bénéficier de l'expérience du CEA LIST sur l'analyse de code binaire et réutiliser certains composants logiciels de OSMOSE. En plus des applications directes au binaire, nous pensons que nos résultats scientifiques pourront avoir des applications à des domaines proches, comme l'analyse de programmes C bas niveau typiquement rencontrés dans les systèmes embarqués et les systèmes d'exploitation.