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
Jakub Szefer’s research interests are at the intersection of computer architecture and hardware security. His research focuses on secure hardware-software architectures for servers and mobile devices, virtualization and cloud security, hardware security verification, physically unclonable functions, and hardware FPGA implementation of cryptographic algorithms. His research is supported through National Science Foundation and industry donations. He joined Yale University in summer 2013 as an Assistant Professor of Electrical Engineering, where he started the Computer Architecture and Security Laboratory (CAS Lab). Prior to joining Yale, he received Ph.D. and M.A. degrees in Electrical Engineering from Princeton University and worked with Prof. Ruby B. Lee on secure hardware architectures. He received B.S. with highest honors in Electrical and Computer Engineering from University of Illinois at Urbana-Champaign.