L'interprète, le JIT et la licorne
Résumé
L'exécution symbolique, une méthode populaire d'analyse de programmes, a du mal à passer à l'échelle sur de gros codes. Outre les traditionnels problèmes d'explosion de chemins et de résolution des prédicats logiques, d'aucuns se plaignent du coût d'interprétation du langage cible et se tournent par conséquent vers la compilation, qu'elle soit statique ou à la volée, pour améliorer les performances. Sceptiques mais non moins curieux, nous saisissons ce prétexte pour rajouter un peu de compilation à la volée dans le moteur d'exécution symbolique de la plateforme BINSEC, écrite en OCaml. Permettez-nous ainsi d'introduire JITPSI, une petite bibliothèque qui tire son inspiration de MetaOCaml et ocaml-jit. JITPSI concourt à compiler harmonieusement en x86-64, directement depuis OCaml, une séquence d'appels de fonctions. Nous utilisons JITPSI pour transformer à la volée l'interpréteur d'arbres syntaxiques abstraits de BINSEC en sous-programmes filetés (threaded code). Notre intention première est ici d'améliorer la résolution du défi de rétro-ingénierie licorne issu du France CyberSecurity Challenge 2022 proposé par l'ANSSI ; soit une accélération d'environ 40%.
Domaines
Informatique [cs]
Origine : Fichiers produits par l'(les) auteur(s)