Please use this identifier to cite or link to this item: https://hdl.handle.net/10356/165417
Title: A formal methodology for verifying side-channel vulnerabilities in cache architectures
Authors: Jiang, Ke
Zhang, Tianwei
Sanan, David
Zhao, Yongwang
Liu, Yang
Keywords: Engineering::Computer science and engineering
Issue Date: 2022
Source: Jiang, K., Zhang, T., Sanan, D., Zhao, Y. & Liu, Y. (2022). A formal methodology for verifying side-channel vulnerabilities in cache architectures. 23rd International Conference on Formal Engineering Methods (ICFEM 2022), 13478, 190-208. https://dx.doi.org/10.1007/978-3-031-17244-1_12
Project: NRF2018 NCR-NCR009-0001 
RS02/19 
NTU-SUG 
Conference: 23rd International Conference on Formal Engineering Methods (ICFEM 2022)
Abstract: 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.
URI: https://hdl.handle.net/10356/165417
ISBN: 978-3-031-17243-4
DOI: 10.1007/978-3-031-17244-1_12
Schools: School of Computer Science and Engineering 
Rights: © 2022 Springer Nature Switzerland AG. All rights reserved. This is a post-peer-review, pre-copyedit version of an article published in Proceedings of 23rd International Conference on Formal Engineering Methods (ICFEM 2022). The final authenticated version is available online at: https://doi.org/10.1007/978-3-031-17244-1_12.
Fulltext Permission: open
Fulltext Availability: With Fulltext
Appears in Collections:SCSE Conference Papers

Files in This Item:
File Description SizeFormat 
2022_ICFEM_cache_evaluation.pdf697.03 kBAdobe PDFThumbnail
View/Open

Page view(s)

137
Updated on Feb 28, 2024

Download(s)

18
Updated on Feb 28, 2024

Google ScholarTM

Check

Altmetric


Plumx

Items in DR-NTU are protected by copyright, with all rights reserved, unless otherwise indicated.