Cache timing side-channel vulnerability checking with computation tree logic
Cache timing side-channel vulnerability checking with computation tree logic
复制标题
DOI：
10.1145/3214292.3214294
复制
发表时间：
2018-06
期刊：
影响因子：
--
通讯作者：
Shuwen Deng;Wenjie Xiong;Jakub Szefer
中科院分区：
文献类型：
--
作者：
Shuwen Deng;Wenjie Xiong;Jakub Szefer
卡车是现代处理器的关键特征之一，因为它们通过最近使用的数据来帮助改善内存访问时机。但是，由于缓存命中和错过之间的时机差异，过去已经发现和利用了许多时机侧通道。在本文中，计算树逻辑用于建模处理器缓存逻辑的执行路径，并为可能导致时机侧通道漏洞的路径得出公式。总共提出了28种类型的缓存攻击：20种映射到先前在文献中分类或讨论的攻击，而8种类型是新的。此外，为了启用实际漏洞检查，我们提出了一种新方法，该方法限制了需要通过计算树逻辑检查需要检查的执行路径的深度，从而可以使用新的模型检查基于计算树逻辑的基于计算的CACHE安全验证三步单孔障碍模型。
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.