​La sécurité logicielle est aujourd'hui une préoccupation majeure. Or, les analyses de sécurité actuelles portent essentiellement sur le code source* des programmes, lequel n'est pas toujours accessible. « Même quand il l'est, son analyse est dans certains cas insuffisante pour détecter des logiciels malveillants ou des bugs introduits par le compilateur » ajoute un chercheur du List, institut de CEA Tech.

Afin de pallier le manque d'outils d'analyse fiables, les chercheurs du List ont mis à profit leur forte expertise en sécurité informatique : ils ont adapté les méthodes formelles, des techniques à l'état de l'art pour l'analyse de code source dans les systèmes critiques, afin de les rendre capables de vérifier le code exécutable des logiciels. « Les méthodes formelles sont sensibles aux comportements du programme, plutôt qu'à la façon dont il est écrit. De plus, elles sont capables d'en explorer tous les comportements, ou au moins une part très significative. » De ce fait, les outils proposés sont plus robustes et plus fiables que les méthodes syntaxiques utilisées par les industriels, lesquelles étudient  de manière simple le code exécutable ou analysent certains comportements de façon aléatoire.

Les outils issus en premier lieu de travaux collaboratifs ont été regroupés pour former la plate-forme d'analyse de code binaire open source BINSEC. Cette dernière a été testée avec succès et sera présentée au salon international Black Hat Europe à la fin de l'année.