|
Evènement pour le groupe Modélisation et Verification
Date | 2010-03-11 11:30-12:45 |
Titre | Static 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.
|
Lieu | Salle 076, LaBRI, Rez-de-chaussée |
Orateur | Johannes Kinder |
Email | kinder@forsyte.de |
Url | TU Darmstadt, Allemagne |
Aucun document lié à cet événement. RetourRetour à l'index
| |