Cache timing side-channel vulnerability checking with computation tree logic

Abstract

Caches are one of the key features of modern processors as they help to improve memory access timing through caching recently used data. However, due to the timing differences between cache hits and misses, numerous timing side-channels have been discovered and exploited in the past. In this paper, Computation Tree Logic is used to model execution paths of the processor cache logic, and to derive formulas for paths that can lead to timing side-channel vulnerabilities. In total, 28 types of cache attacks are presented: 20 types of which map to attacks previously categorized or discussed in literature, and 8 types are new. Furthermore, to enable practical vulnerability checking, we present a new approach that limits the depth of the execution paths that need to be checked by the Computation Tree Logic, allowing for use of bounded model checking for Computation Tree Logic based cache security verification using the new three-step single-cache-block-access model.