Abstract
Compiling a source program into machine code can make it more resistant to certain attacks. However, many semantically correct compilation optimizations can weaken program security. We'll look at how to characterize these security differences between a source program fragment and its compiled code, using classic semantic tools: observational equivalence and the full abstraction problem. We will present some approaches that have been proposed to compile while preserving observational equivalence.
