Analyse d'exécutables x86 par transformation sous forme de clauses de Horn

Résumé

Intel et AMD sont les leaders mondiaux quant à la production de processeurs,
à la fois destinés aux ordinateurs personnels qu’aux serveurs industriels. Ils représentent
à eux seuls plus de 90% de la part du marché mondial.
De ce constat, il en va de soi que la majorité des programmes et logiciels
implémentés en langage de haut niveau soient compilés en vue de s’exécuter sur
des processeurs Intel et AMD. Comme ces processeurs partagent la même architecture
(x86), il serait donc intéressant de pouvoir étudier et réaliser diverses
analyses de programmes sur ces programmes exécutables mais paradoxalement,
ceci reste assez complexe et très peu d’études existent à ce sujet.
Cela s’explique en grande partie par le fait que ces processeurs se doivent
d’être rétrocompatibles entre eux. En effet, un programme s’exécutant sur un
processeur Intel Pentium 4 (2000) doit également pouvoir s’exécuter sur un Intel
Core i7 (2008). Cela signifie que le jeu d’instructions qu’exécutent les processeurs
actuels doit contenir les instructions utilisées par les processeurs précédents.
Cette architecture de jeu d’instructions est le code machine x86 et les
programmes exécutables sur des processeurs compatibles avec ce jeu d’instructions
sont dits exécutables x86.
L’intérêt de ce mémoire est de rendre possible ou de simplifier l’application
d’analyses de programmes sur des programmes exécutables x86. L’approche que
nous proposons est d’élaborer et de concevoir une méthode de traduction en
clauses de Horn et plus précisément en programmation logique par contraintes.
L’avantage des clauses de Horn est qu’elles bénéficient d’un large ensemble
d’analyses de programmes réalisées à leur sujet et qu’elles s’y prêtent particulièrement
bien. La technique mise au point et expliquée dans ce mémoire se
base sur une traduction séquentielle des instructions du code machine x86 en
leur équivalent en clauses de Horn.

la date de réponse	26 juin 2017
langue originale	Français
L'institution diplômante	Universite de Namur
Superviseur	Anthony Cleve (Président) & Wim Vanhoof (Promoteur)