The Correctness-Security Gap in Compiler Optimization

Explore the critical issue of the correctness-security gap in compiler optimization through this 25-minute IEEE conference talk. Delve into how standard compiler optimizations, despite being formally proven correct, can inadvertently violate security guarantees present in source code while preserving functionality. Examine concrete code examples illustrating this phenomenon and analyze why it occurs, focusing on the limitations of current techniques that model program state but not machine state. Gain insights into a proposed research agenda aimed at identifying, understanding, and mitigating security errors introduced by compiler optimizations, encompassing areas such as testing, program analysis, theorem proving, and the development of more accurate machine models for assessing optimization impacts on security.