Abstract Interpretation under Speculative Execution

TL;DR

This paper presents a sound static analysis method for programs with speculative execution, enhancing accuracy in execution time estimation and side channel detection by modeling speculative behaviors.

Contribution

It introduces virtual control flow and optimization techniques to make abstract interpretation sound and efficient under speculative execution.

Findings

Outperforms existing abstract interpretation methods in accuracy.

Successfully applied to static cache analysis for timing and security.

Ensures soundness of analysis in the presence of speculative execution.

Abstract

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.