세미나

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 to leak sensitive information.  Most recently, Spectre and Meltdown attacks have re-ignited interest in side-channel attacks. Especially, they have shown how side channels, combined with speculative execution, can be used exfiltrate sensitive information in modern processors.  To prevent timing side-channel attacks, numerous secure caches have been developed.  However, there is no formal verification framework to show that these caches are indeed secure.  This presentation will discuss how temporal logic can be used to model execution paths of the processor cache logic, and to derive temporal logic formulas for paths that can lead to timing side-channel vulnerabilities.  Once the logic formulas are derived, they can be used to check whether a cache design is susceptible to a potential attack. To overcome search space explosion problem, this presentation will show how a new three-step model can be used to limit the search space.  Further, based on exhaustive enumeration of all possible three-step access patterns, a number of potentially new types of cache side-channel attacks will be discussed