Title: 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.