CANAL: A Cache Timing Analysis Framework via LLVM Transformation
CANAL: A Cache Timing Analysis Framework via LLVM Transformation
复制标题
DOI：
10.1145/3238147.3240485
复制
发表时间：
2018-07
期刊：
影响因子：
--
通讯作者：
Chungha Sung;Brandon Paulsen;Chao Wang
中科院分区：
文献类型：
--
作者：
Chungha Sung;Brandon Paulsen;Chao Wang
一个统一的建模框架的非功能特性的程序是必不可少的软件分析和验证的研究，因为它减少了负担，个人研究人员实施新的方法和比较现有的方法。我们提出CANAL，一个框架，模型的该高速缓存行为的程序，通过转换其中间表示在LLVM编译器。CANAL插入辅助变量和指令，以允许标准验证工具处理一类新的高速缓存相关属性，例如，用于计算最坏情况下的执行时间和检测侧通道泄漏。我们使用三种验证工具：KLEE，SMACK和Crab-llvm证明了CANAL的有效性。我们确认我们的缓存模型的准确性，通过比较与CPU周期准确的模拟结果GEM 5。
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 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. We demonstrate the effectiveness of CANAL using three verification tools: KLEE, SMACK and Crab-llvm. We confirm the accuracy of our cache model by comparing with CPU cycle-accurate simulation results of GEM5.