Compiler Optimizations with Retrofitting Transformations: Is there a Semantic Mismatch?

Jay P. Lim, Vinod Ganapathy, Santosh Nagarakatte.

Proceedings of the 12th ACM SIGSAC Workshop on Programming Languages and Analysis for Security (PLAS 2017); Dallas, Texas, USA; October 30, 2017.

A retrofitting transformation modifies an input program by adding instrumentation to monitor security properties at runtime. These tools often transform the input program in complex ways. Compiler optimizations can erroneously remove the instrumentation added by a retrofitting transformation in the presence of semantic mismatches between the assumptions of retrofitting transformations and compiler optimizations. This paper proposes a strategy to ascertain that every event of interest that is checked in the retrofitted program is also checked after optimizations. Our initial experiments have identified bugs both in previously proposed retrofitting transformations and our implementations of retrofitting transformations.

Paper: [ PDF ] (© ACM)
Slides: [ PDF ]
DOI: [ 10.1145/3139337.3139343 ]

Papers page