A formal methodology for verifying side-channel vulnerabilities in cache architectures

• Main Authors: Jiang, Ke, Zhang, Tianwei, Sanan, David, Zhao, Yongwang, Liu, Yang
• Other Authors: School of Computer Science and Engineering
• Format: Conference or Workshop Item
• Language: English
• Published: 2023
• Subjects: Engineering::Computer science and engineering; Cache Designs; Side-Channel Attacks; Security Verification
• Online Access: https://hdl.handle.net/10356/165417
• Institution: Nanyang Technological University

Security-aware CPU caches have been designed to mitigate side-channel attacks and prevent information leakage. How to validate the effectiveness of these designs remains an unsolved problem. Prior works assess the security of architectures empirically without a formal guarantee, making the evaluation results less convincing. In this paper, we propose a comprehensive methodology based on formal methods for security verification of cache architectures. Specifically, we design an entropy-based noninterference reasoning framework with two unwinding conditions to assess the information leakage of the cache designs. The reasoning framework quantifies the dependency relationships by the mutual information between the distributions of input and output of side channels. Given a cache design, we formalize its behavior specification along with the cache layouts into an abstract state machine, to instantiate the parameterized reasoning framework that discloses any potential vulnerabilities. We use our methodology to assess eight state-of-the-art cache architectures to demonstrate reliability as well as flexibility.