Verifying cache architecture vulnerabilities using a formal security verification flow. (April 2021)

• Record Type: Journal Article
• Authors: Ghasempouri, Tara; Raik, Jaan; Paul, Kolin; Reinbrecht, Cezar; Hamdioui, Said; Mottaqiallah,
• Is Part Of: Microelectronics and reliability. Volume 119(2021)
• Publication Date: 2021-04
• Subjects: Side-channel attacks -- Security verification -- Cache attacks -- Cache security -- Formal verification; Electronic apparatus and appliances -- Reliability -- Periodicals; Miniature electronic equipment -- Periodicals; Appareils électroniques -- Fiabilité -- Périodiques; Équipement électronique miniaturisé -- Périodiques; Electronic apparatus and appliances -- Reliability; Miniature electronic equipment; Periodicals; 621.3815
• DOI: 10.1016/j.microrel.2021.114085
• Languages: English
• ISSNs: 0026-2714

Abstract

Abstract: 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. Highlights: Formal verification Cache Vulnerabilities Security requirement Security Cache verification template