Abstract
Compiling a source program in machine code can be an opportunity to make it more resistant to certain attacks. For example, systematic bounds tests when accessing arrays can be introduced during compilation, then optimized to reduce the runtime overhead, thus greatly increasing security at reasonable cost. However, many compilation optimizations, even though semantically correct, can weaken program security. This is particularly true of optimizations that assume the absence of undefined behaviors in the source program. We have shown 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 present some recently proposed approaches to compiling " securely ", i.e. preserving observational equivalence in both directions.
