The Correctness-Security Gap in Compiler Optimization
Venue
Security and Privacy Workshops (SPW), 2015 IEEE, IEEE, pp. 73-87
Publication Year
2015
Authors
Vijay D'Silva, Mathias Payer, Dawn Song
BibTeX
Abstract
There is a significant body of work devoted to testing, verifying, and certifying
the correctness of optimizing compilers. The focus of such work is to determine if
source code and optimized code have the same functional semantics. In this paper,
we introduce the correctness-security gap, which arises when a compiler
optimization preserves the functionality of but violates a security guarantee made
by source code. We show with concrete code examples that several standard
optimizations, which have been formally proved correct, in-habit this
correctness-security gap. We analyze this gap and conclude that it arises due to
techniques that model the state of the program but not the state of the underlying
machine. We propose a broad research programme whose goal is to identify,
understand, and mitigate the impact of security errors introduced by compiler
optimizations. Our proposal includes research in testing, program analysis, theorem
proving, and the development of new, accurate machine models for reasoning about
the impact of compiler optimizations on security.
