CANAL: a cache timing analysis framework via LLVM transformation

Chungha Sung, Brandon Paulsen, Chao Wang

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.

BibTeX

@inproceedings{Sung-al:ASE18,
  author    = {Chungha Sung and
               Brandon Paulsen and
               Chao Wang},
  title     = {{CANAL:} a cache timing analysis framework via {LLVM} transformation},
  booktitle = {ASE},
  pages     = {904--907},
  publisher = {{ACM}},
  year      = {2018},
}

CANAL: a cache timing analysis framework via LLVM transformation

Abstract

Related papers