Enhancing side-channel security: detection, mitigation and verification
In the realm of computer security, side-channel attacks pose a significant threat by exploiting subtle information leaks during the operation of a system. These attacks, which include cache side-channel attacks, a particularly insidious subset, enable adversaries to extract sensitive data by exploit...
| Main Author: | |
|---|---|
| Other Authors: | |
| Format: | Thesis-Doctor of Philosophy |
| Language: | English |
| Published: |
Nanyang Technological University
2025
|
| Subjects: | |
| Online Access: | https://hdl.handle.net/10356/182903 |
| _version_ | 1826124063285706752 |
|---|---|
| author | Jiang, Ke |
| author2 | Zhang Tianwei |
| author_facet | Zhang Tianwei Jiang, Ke |
| author_sort | Jiang, Ke |
| collection | NTU |
| description | In the realm of computer security, side-channel attacks pose a significant threat by exploiting subtle information leaks during the operation of a system. These attacks, which include cache side-channel attacks, a particularly insidious subset, enable adversaries to extract sensitive data by exploiting cache memory behaviors. To defeat cache side-channel attacks, current research has made strides in developing software and hardware-level countermeasures, but challenges persist in achieving comprehensive and scalable methods. Furthermore, constant-time coding practices, effective against traditional cache-based side channels, face limitations with emerging threats like ciphertext side channels. Additionally, new micro-architectural designs, e.g., cache designs, lack formal guarantees of effectiveness, highlighting the need for ongoing evaluation and adaptability. This thesis addresses these challenges, with the aim of improving cache side-channel defense methods, addressing emerging ciphertext side channels, and improving the security of novel hardware designs through formal verification.
To be more specific, this thesis focuses on three primary objectives. First, it aims to advance cache side-channel detection by developing comprehensive methods to identify and mitigate vulnerabilities in cryptography software. Second, it addresses the emerging threat of ciphertext side channels by proposing a holistic approach that combines constant-time coding practices with compiler-aided mitigation mechanisms. Finally, the research seeks to enhance the security of new cache designs by providing a means for formal verification, acknowledging the challenges posed by their complexity and potential vulnerabilities. Through these endeavors, this thesis contributes to fortifying the security of modern computing systems against the evolving and increasingly sophisticated landscape of side-channel threats.
We present three significant contributions addressing side-channel vulnerabilities. Firstly, we introduce CaType, a groundbreaking refinement type-based tool for cache side-channel detection in cryptographic software. CaType analyzes x86 assembly code using refinement types, offering enhancements like bit-level granularity tracking, precise type inferences, and high scalability. It is the first static analyzer for cryptography libraries considering blinding-based defenses and utilizes cache layouts to suppress false positives, demonstrating superior performance in identifying vulnerabilities. Secondly, we propose CipherGuard, a compiler-aided mitigation tool addressing ciphertext side channels by recognizing secret-dependent store instructions and providing multiple strategies to protect these instructions. For the first time, CipherGuard employs various precise and flexible mitigation variants based on the LLVM ecosystem, achieving security without hardware modification and displaying enhanced efficiency in cryptography implementations compared to existing defense tools. Lastly, we introduce a formal methodology for security verification of cache architectures, employing an entropy-based noninterference reasoning framework to assess information leakage. The methodology, applied to eight cache architectures, demonstrates reliability and flexibility, contributing to the advancement of cache side-channel security. |
| first_indexed | 2025-03-09T13:40:17Z |
| format | Thesis-Doctor of Philosophy |
| id | ntu-10356/182903 |
| institution | Nanyang Technological University |
| language | English |
| last_indexed | 2025-03-09T13:40:17Z |
| publishDate | 2025 |
| publisher | Nanyang Technological University |
| record_format | dspace |
| spelling | ntu-10356/1829032025-03-06T04:35:55Z Enhancing side-channel security: detection, mitigation and verification Jiang, Ke Zhang Tianwei College of Computing and Data Science tianwei.zhang@ntu.edu.sg Computer and Information Science In the realm of computer security, side-channel attacks pose a significant threat by exploiting subtle information leaks during the operation of a system. These attacks, which include cache side-channel attacks, a particularly insidious subset, enable adversaries to extract sensitive data by exploiting cache memory behaviors. To defeat cache side-channel attacks, current research has made strides in developing software and hardware-level countermeasures, but challenges persist in achieving comprehensive and scalable methods. Furthermore, constant-time coding practices, effective against traditional cache-based side channels, face limitations with emerging threats like ciphertext side channels. Additionally, new micro-architectural designs, e.g., cache designs, lack formal guarantees of effectiveness, highlighting the need for ongoing evaluation and adaptability. This thesis addresses these challenges, with the aim of improving cache side-channel defense methods, addressing emerging ciphertext side channels, and improving the security of novel hardware designs through formal verification. To be more specific, this thesis focuses on three primary objectives. First, it aims to advance cache side-channel detection by developing comprehensive methods to identify and mitigate vulnerabilities in cryptography software. Second, it addresses the emerging threat of ciphertext side channels by proposing a holistic approach that combines constant-time coding practices with compiler-aided mitigation mechanisms. Finally, the research seeks to enhance the security of new cache designs by providing a means for formal verification, acknowledging the challenges posed by their complexity and potential vulnerabilities. Through these endeavors, this thesis contributes to fortifying the security of modern computing systems against the evolving and increasingly sophisticated landscape of side-channel threats. We present three significant contributions addressing side-channel vulnerabilities. Firstly, we introduce CaType, a groundbreaking refinement type-based tool for cache side-channel detection in cryptographic software. CaType analyzes x86 assembly code using refinement types, offering enhancements like bit-level granularity tracking, precise type inferences, and high scalability. It is the first static analyzer for cryptography libraries considering blinding-based defenses and utilizes cache layouts to suppress false positives, demonstrating superior performance in identifying vulnerabilities. Secondly, we propose CipherGuard, a compiler-aided mitigation tool addressing ciphertext side channels by recognizing secret-dependent store instructions and providing multiple strategies to protect these instructions. For the first time, CipherGuard employs various precise and flexible mitigation variants based on the LLVM ecosystem, achieving security without hardware modification and displaying enhanced efficiency in cryptography implementations compared to existing defense tools. Lastly, we introduce a formal methodology for security verification of cache architectures, employing an entropy-based noninterference reasoning framework to assess information leakage. The methodology, applied to eight cache architectures, demonstrates reliability and flexibility, contributing to the advancement of cache side-channel security. Doctor of Philosophy 2025-03-06T04:35:55Z 2025-03-06T04:35:55Z 2024 Thesis-Doctor of Philosophy Jiang, K. (2024). Enhancing side-channel security: detection, mitigation and verification. Doctoral thesis, Nanyang Technological University, Singapore. https://hdl.handle.net/10356/182903 https://hdl.handle.net/10356/182903 en This work is licensed under a Creative Commons Attribution-NonCommercial 4.0 International License (CC BY-NC 4.0). application/pdf Nanyang Technological University |
| spellingShingle | Computer and Information Science Jiang, Ke Enhancing side-channel security: detection, mitigation and verification |
| title | Enhancing side-channel security: detection, mitigation and verification |
| title_full | Enhancing side-channel security: detection, mitigation and verification |
| title_fullStr | Enhancing side-channel security: detection, mitigation and verification |
| title_full_unstemmed | Enhancing side-channel security: detection, mitigation and verification |
| title_short | Enhancing side-channel security: detection, mitigation and verification |
| title_sort | enhancing side channel security detection mitigation and verification |
| topic | Computer and Information Science |
| url | https://hdl.handle.net/10356/182903 |
| work_keys_str_mv | AT jiangke enhancingsidechannelsecuritydetectionmitigationandverification |