Paper Info
Title
The Correctness-Security Gap in Compiler Optimization
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.
Year
DOI
Venue
2015
10.1109/SPW.2015.33
2015 IEEE Security and Privacy Workshops
Keywords
Field
DocType
compiler optimization,formal correctness,security
Dead code elimination,Interprocedural optimization,Programming language,Loop-invariant code motion,Computer science,Compiler correctness,Compiler,Optimizing compiler,Compiler construction,Superoptimization
Conference
Citations 
PageRank 
References 
20
0.90
30
Authors
3
Name
Order
Citations
PageRank
Vijay D'Silva123914.07
Mathias Payer274243.10
Dawn Song37084442.36