Leveraging LLVM's ScalarEvolution for Symbolic Data Cache Analysis
Valentin Touzeau, Jan Reineke
Abstract
While instruction cache analysis is essentially a solved problem, data cache analysis is more challenging. In contrast to instruction fetches, the data accesses generated by a memory instruction may vary with the program's inputs and across dynamic occurrences of the same instruction in loops.
We observe that the plain control-flow graph (CFG) abstraction employed in classical cache analyses is inadequate to capture the dynamic behavior of memory instructions. On top of plain CFGs, accurate analysis of the underlying program's cache behavior is impossible.
Thus, our first contribution is the definition of a more expressive program abstraction coined symbolic control-flow graphs, which can be obtained from LLVM's ScalarEvolution analysis. To exploit this richer abstraction, our main contribution is the development of symbolic data cache analysis, a smooth generalization of classical LRU must analysis from plain to symbolic control-flow graphs.
The experimental evaluation demonstrates that symbolic data cache analysis consistently outperforms classical LRU must analysis both in terms of accuracy and analysis runtime.
Ask about this paper
Your agent reads all of it.
Lune indexed this paper to the last equation, along with the top-tier papers that cite it. Ask a question and the answer quotes them.
Builds on2
Related papers
- SYMSAN: Time and Space Efficient Concolic Execution via Dynamic Data-flow AnalysisJu Chen, Wookhyun Han, Mingjun Yin, Haochen Zeng et al.USENIX Security 2022
- SpecuSym: speculative symbolic execution for cache timing leak detectionShengjian Guo, Yueqi Chen, Peng Li, Yueqiang Cheng et al.ICSE 2020 · 34 citations
- CaSym: Cache Aware Symbolic Execution for Side Channel Detection and MitigationRobert Brotzman, Shen Liu, Danfeng Zhang, Gang Tan et al.S&P 2019 · 77 citations
- Rapid: Region-Based Pointer DisambiguationKhushboo Chitre, Piyus Kedia, Rahul PurandareOOPSLA 2023 · 2 citations
- Validation of Abstract Side-Channel Models for Computer ArchitecturesHamed Nemati, Pablo Buiras, Andreas Lindner, Roberto Guanciale et al.CAV 2020 · 18 citations
