Quelques lignes d’instructions dissimulées dans un logiciel : il n’en faut pas plus pour corrompre la sécurité d’un système. Au centre Inria Rennes-Bretagne Atlantique, une équipe de recherche étudie comment des méthodes formelles pourraient permettre une analyse du code binaire afin d’en améliorer la lisibilité et ainsi mieux repérer les programmes malveillants qui s’y cacheraient. Ces travaux sont menés avec DGA Maîtrise de l’information, l’établissement rennais de la Direction générale de l’armement (DGA).

Ils détruisent des disques durs. S’infiltrent. Espionnent. Dérobent des numéros de cartes bleues. Subtilisent des mots de passe. Ou modifient subrepticement la vitesse de rotation de centrifugeuses industrielles. Dans un monde hyper-connecté, les vers, virus, chevaux de Troie et autres malware constituent une menace en rien virtuelle.

Pour les chercheurs, le défi consiste à prendre ce code abscons, à l’analyser au moyen de méthodes formelles afin d’en proposer une représentation de plus haut niveau. Avec à la clé l’espoir de parvenir à automatiser cette analyse. “Mais nous n’en sommes pas là, explique l’Inria. Au préalable, il faudra lever beaucoup de verrous. C’est encore une recherche en amont. Nous avons identifié là un problème qui intéresse à la fois Inria et DGA Maîtrise de l’information. Nous mettons ensemble nos moyens pour faire avancer nos connaissances sur le sujet.”

Un autre aspect de ces travaux porte sur les techniques d’obfuscation de code. Autrement dit les mille et une façons de rendre la lecture d’un programme véritablement ésotérique. Ces méthodes sont utilisées par les créateurs de virus, mais elles servent aussi à protéger les logiciels licites contre les malveillances.

Les éditeurs de jeux vidéo, par exemple, y recourent pour empêcher les pirates de produire des contrefaçons. Dans d’autres domaines, comme les télécommunications, les constructeurs s’en servent aussi pour protéger des secrets industriels sur des technologies propriétaires.