Metadata
| Year | 2018 |
|---|---|
| Target | LLVM IR |
| Technique | Formal |
| Guarantees | sound |
| Available | yes |
| Repository | https://github.com/canalcache/canal |
| Paper1 | 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 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.