CANAL: A Cache Timing Analysis Framework via LLVM Transformation
Abstract
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. 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. CANAL is available on GitHub and YouTube.
Cite
@article{arxiv.1807.03329,
title = {CANAL: A Cache Timing Analysis Framework via LLVM Transformation},
author = {Chungha Sung and Brandon Paulsen and Chao Wang},
journal= {arXiv preprint arXiv:1807.03329},
year = {2018}
}