Increasing the performance of symbolic execution by compiling symbolic handling into binaries

Exécution symbolique haute performance par la compilation du moteur symbolique dans le programme testé L'exécution symbolique a le potentiel de rendre les logiciels plus sûrs en améliorant considérablement la recherche automatisée des vulnérabilités. Nous proposons une technique générale qui permet des implémentations plus efficaces de la composante d'exécution dans les exécuteurs symboliques. Nous examinons d'abord l'état de l'art. A partir des résultats de cette comparaison, nous dérivons l'idée d'accélérer l'exécution en intégrant la manipulation symbolique dans les programmes compilés au lieu d'interpréter symboliquement une représentation de plus haut niveau du programme testé. En utilisant cette approche, nous développons un exécuteur symbolique basé sur le compilateur et nous montrons qu'il atteint effectivement une vitesse d'exécution élevée par rapport aux systèmes actuellement les plus performants. Comme le compilateur est limité aux scénarios où le code source du programme testé est disponible, nous concevons et mettons en œuvre une solution complémentaire pour l'exécution symbolique des binaires ; elle utilise la même idée de base d'intégration de l'exécution symbolique dans un code machine rapide, mais combine l'approche avec la traduction binaire pour relever les défis de l'analyse binaire seule. Nous concluons en discutant des directions de recherche qui pourraient conduire à des systèmes encore plus pratiques.