A formal methodology for verifying side-channel vulnerabilities in cache architectures
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 evaluatio...
Saved in:
| Main Authors: | , , , , |
|---|---|
| Other Authors: | |
| Format: | Conference or Workshop Item |
| Language: | English |
| Published: |
2023
|
| Subjects: | |
| Online Access: | https://hdl.handle.net/10356/165417 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| Institution: | Nanyang Technological University |
| Language: | English |
| Summary: | 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. |
|---|