一句话：提出 CANAL，通过 LLVM IR 变换将缓存行为编码为辅助变量与指令，使标准验证工具能分析缓存时序属性。
论文提出 CANAL，一个用于程序非功能属性的统一建模框架，旨在减轻研究者实现新方法和比较现有方法的工作量。它针对缓存行为建模：在 LLVM 编译器的中间表示上插入辅助变量及操作这些变量的指令，将原本隐含的缓存状态与访问时序显式化，使标准验证工具能够处理一类新的缓存相关属性。该方法可用于计算最坏情况执行时间（WCET）和检测侧信道泄漏。摘要未给出具体实验评估，仅以这两类应用说明框架的适用性。
A unified modeling framework for non-functional properties of a program is essential for research in software analysis and verification, since it reduces burdens on individual researchers to implement new approaches and compare existing approaches. We present CANAL, a framework that models the cache behaviors of a program by transforming its intermediate representation in the LLVM compiler. CANAL inserts auxiliary variables and instructions over these variables, to allow standard verification tools to handle a new class of cache related properties, e.g., for computing the worst-case execution time and detecting side-channel leaks.
DOI 原文 ·
@inproceedings{paperbot4741,
title = {CANAL: a cache timing analysis framework via LLVM transformation},
author = {Chungha Sung and Brandon Paulsen and Chao Wang},
booktitle = {ASE},
year = {2018},
doi = {10.1145/3238147.3240485}
}