Analyzing the behavior of a program running on a processor that supports speculative execution is crucial for applications such as execution time estimation and side channel detection. Unfortunately, existing static analysis techniques based on abstract interpretation do not model speculative execution since they focus on functional properties of a program while speculative execution does not change the functionality. To fill the gap, we propose a method to make abstract interpretation sound under speculative execution. There are two contributions. First, we introduce the notion of virtual control flow to augment instructions that may be speculatively executed and thus affect subsequent instructions. Second, to make the analysis efficient, we propose optimizations to handle merges and loops and to safely bound the speculative execution depth. We have implemented and evaluated the proposed method in a static cache analysis for execution time estimation and side channel detection. Our experiments show that the new method, while guaranteed to be sound under speculative execution, outperforms state-of-the-art abstract interpretation techniques that may be unsound.
Tue 25 JunDisplayed time zone: Tijuana, Baja California change
14:00 - 15:30 | Static AnalysisPLDI Research Papers at 229AB Chair(s): Martin C. Rinard Massachusetts Institute of Technology | ||
14:00 20mTalk | Abstract Interpretation under Speculative Execution PLDI Research Papers Media Attached | ||
14:20 20mTalk | A Fast Analytical Model of Fully Associative Caches PLDI Research Papers Tobias Gysi ETH Zurich, Switzerland, Tobias Grosser ETH Zurich, Laurin Brandner ETH Zurich, Switzerland, Torsten Hoefler ETH Zurich Media Attached | ||
14:40 20mTalk | Sound, Fine-Grained Traversal Fusion for Heterogeneous Trees PLDI Research Papers Laith Sakka Purdue University, Kirshanthan Sundararajah Purdue University, Ryan R. Newton Indiana University, Milind Kulkarni Purdue University Media Attached | ||
15:00 20mTalk | Size-Change Termination as a Contract PLDI Research Papers Phúc C. Nguyễn University of Maryland, Thomas Gilray University of Maryland, Sam Tobin-Hochstadt Indiana University, David Van Horn University of Maryland, USA Media Attached |