SCAFinder: Formal Verification of Cache Fine-Grained Features for Side Channel Detection

Recent research has unveiled numerous cache-timing side-channel attacks exploiting the side effects of fine-grained cache features, such as coherence protocol and prefetch, among others. Traditional modeling methods and verification techniques are insufficient for verifying caches with fine-grained features and detecting cache timing vulnerabilities. There is a necessity for comprehensive verification of such complex cache designs. This paper presents SCAFinder, a verification framework targeting the cache designs with fine-grained features; it identifies cache side-channel attacks through model checking techniques. Specifically, it proposes a modeling methodology for cache designs that enables us to abstract the cache's behavior and latency characteristics. We implement a search algorithm for finding all counterexamples based on open-source model checking software. Subsequently, we add an attack scenario analysis module to discover attacks applicable to specific scenarios. We evaluate SCAFinder on Intel Skylake-X microarchitecture, demonstrating its capability to generate 7 new attack sequences exploiting coherence protocol and prefetch, and 12 new replacement policy-based side channels. As a case study, we successfully built a covert channel for one of the sequences on the real-world processor. To the best of our knowledge, we are the first to implement cross-core replacement policy-based attacks on non-inclusive caches.