|
What You See Is Not What You eXecute: computers do not execute source-code
programs; they execute machine-code programs that are generated from source
code. Not only can the WYSINWYX phenomenon create a mismatch between what a
programmer intends and what is actually executed by the processor, it can
cause analyses that are performed on source code to fail to detect certain
bugs and security vulnerabilities. This issue arises regardless of whether
one's favorite approach to assuring that programs behave as desired is based
on theorem proving, model checking, or abstract interpretation.
To address the WYSINWYX problem, we have developed a static-analysis
algorithm to recover information from stripped executables about the
memory-access operations that the program performs. This algorithm has been
incorporated into CodeSurfer/x86, a prototype tool for browsing, inspecting,
and analyzing stripped x86 executables.
Joint work with G. Balakrishnan (UW), J. Lim (UW), and T. Teitelbaum
(Cornell and GrammaTech, Inc.).
|