Projet ANR-08-SEGI-0006 – BINCOA : Techniques symboliques  pour l'analyse de code binaire
Programme : Systèmes Embarqués et Grandes Infrastructures (ARPEGE) 2008
Année de financement : 2008
Coordinateur du projet : Monsieur BARDIN Sebastien (COMMISSARIAT A L'ENERGIE ATOMIQUE - CENTRE D'ETUDES NUCLEAIRES SACLAY)
Partenaires : Centre national de la recherche scientifique; Commissariat à l'énergie atomique et aux énergies alternatives; Entreprise autre que TPE ou PME; Entreprise autre que TPE ou PME; PME; Université de Bordeaux
Montant : 883532.0 euros
Date de début : 2009
Durée : 36 mois
Résumé : 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.