WYSINWYX: What You See Is Not What You eXecute
Gogul Balakrishnan and
Thomas W. Reps and
David Melski and
Tim Teitelbaum
Abstract:
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
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.
Paper available as: [PDF]
[Official Version]