Evènement pour le groupe Modélisation et Verification


Date 2010-03-11  11:30-12:45
TitreStatic Analysis of x86 Executables 
RésuméDue to indirect branch instructions, analyses on executables commonly suffer from the problem that a complete control flow graph of the program is not available. Data flow analysis has been proposed before to statically determine branch targets in many cases, yet a generic strategy without assumptions on compiler idioms or debug information was missing. We have devised a framework for generic low level programs with indirect jumps which safely combines a pluggable abstract domain with the notion of partial control flow graphs. Using our framework, we were able to show that the control flow reconstruction algorithm of our disassembly tool Jakstab produces the most precise overapproximation of the control flow graph with respect to the used abstract domain. Based on this rigorous approach to disassembly, Jakstab has evolved into a flexible program analysis framework on binaries. Preliminary experiments with Windows driver binaries show that it can successfully check API specifications with higher precision than existing approaches, while achieving complete independence from source code.  
LieuSalle 076, LaBRI, Rez-de-chaussée 
OrateurJohannes Kinder 
Emailkinder@forsyte.de 
UrlTU Darmstadt, Allemagne 



Aucun document lié à cet événement.

Retour
Retour à l'index