Verifying cache architecture vulnerabilities using a formal security verification flow

Caches form a key feature of modern processors as they help to improve memory access timing by exploiting temporal and spatial data locality. However, the timing differences between cache hits and misses may lead to security vulnerabilities as they can be exploited by logical side channels. In this paper, we propose an innovative and coherent verification methodology to formally verifies cache designs against the potential existence of cache side channel vulnerabilities. Our methodology has been applied to three different cache models, i.e., a conventional cache, a static partitioned cache and a dynamic partitioned cache. The vulnerabilities of these caches have been evaluated using 28 different cache attack types. Results show that our proposed verification method can be applied successfully in verifying whether a cache is vulnerable to side channel attacks or not.