Verification of serialising instructions for security against transient execution attacks
Abstract Transient execution attacks such as Spectre and Meltdown exploit speculative execution in modern microprocessors to leak information via cache side‐channels. Software solutions to defend against many transient execution attacks employ the lfence serialising instruction, which does not allow...
Saved in:
| Main Authors: | , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Wiley
2023-07-01
|
| Series: | IET Computers & Digital Techniques |
| Subjects: | |
| Online Access: | https://doi.org/10.1049/cdt2.12058 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1832547402021601280 |
|---|---|
| author | Kushal K. Ponugoti Sudarshan K. Srinivasan Nimish Mathure |
| author_facet | Kushal K. Ponugoti Sudarshan K. Srinivasan Nimish Mathure |
| author_sort | Kushal K. Ponugoti |
| collection | DOAJ |
| description | Abstract Transient execution attacks such as Spectre and Meltdown exploit speculative execution in modern microprocessors to leak information via cache side‐channels. Software solutions to defend against many transient execution attacks employ the lfence serialising instruction, which does not allow instructions that come after the lfence to execute out‐of‐order with respect to instructions that come before the lfence. However, errors and Trojans in the hardware implementation of lfence can be exploited to compromise the software mitigations that use lfence. The aforementioned security gap has not been identified and addressed previously. The authors provide a formal method solution that addresses the verification of lfence hardware implementation. The authors also show how hardware Trojans can be designed to circumvent lfence and demonstrate that their verification approach will flag such Trojans as well. The authors have demonstrated the efficacy of our approach using RSD, which is an open source RISC‐V based superscalar out‐of‐order processor. |
| format | Article |
| id | doaj-art-fca31bd06a19419382014f733f4f74f0 |
| institution | Kabale University |
| issn | 1751-8601 1751-861X |
| language | English |
| publishDate | 2023-07-01 |
| publisher | Wiley |
| record_format | Article |
| series | IET Computers & Digital Techniques |
| spelling | doaj-art-fca31bd06a19419382014f733f4f74f02025-02-03T06:45:12ZengWileyIET Computers & Digital Techniques1751-86011751-861X2023-07-01173-412714010.1049/cdt2.12058Verification of serialising instructions for security against transient execution attacksKushal K. Ponugoti0Sudarshan K. Srinivasan1Nimish Mathure2Electrical and Computer Engineering North Dakota State University Fargo North Dakota USAElectrical and Computer Engineering North Dakota State University Fargo North Dakota USAElectrical and Computer Engineering North Dakota State University Fargo North Dakota USAAbstract Transient execution attacks such as Spectre and Meltdown exploit speculative execution in modern microprocessors to leak information via cache side‐channels. Software solutions to defend against many transient execution attacks employ the lfence serialising instruction, which does not allow instructions that come after the lfence to execute out‐of‐order with respect to instructions that come before the lfence. However, errors and Trojans in the hardware implementation of lfence can be exploited to compromise the software mitigations that use lfence. The aforementioned security gap has not been identified and addressed previously. The authors provide a formal method solution that addresses the verification of lfence hardware implementation. The authors also show how hardware Trojans can be designed to circumvent lfence and demonstrate that their verification approach will flag such Trojans as well. The authors have demonstrated the efficacy of our approach using RSD, which is an open source RISC‐V based superscalar out‐of‐order processor.https://doi.org/10.1049/cdt2.12058computer architectureelectronic design automationformal verificationintegrated circuit designlogic designmicrocomputers |
| spellingShingle | Kushal K. Ponugoti Sudarshan K. Srinivasan Nimish Mathure Verification of serialising instructions for security against transient execution attacks IET Computers & Digital Techniques computer architecture electronic design automation formal verification integrated circuit design logic design microcomputers |
| title | Verification of serialising instructions for security against transient execution attacks |
| title_full | Verification of serialising instructions for security against transient execution attacks |
| title_fullStr | Verification of serialising instructions for security against transient execution attacks |
| title_full_unstemmed | Verification of serialising instructions for security against transient execution attacks |
| title_short | Verification of serialising instructions for security against transient execution attacks |
| title_sort | verification of serialising instructions for security against transient execution attacks |
| topic | computer architecture electronic design automation formal verification integrated circuit design logic design microcomputers |
| url | https://doi.org/10.1049/cdt2.12058 |
| work_keys_str_mv | AT kushalkponugoti verificationofserialisinginstructionsforsecurityagainsttransientexecutionattacks AT sudarshanksrinivasan verificationofserialisinginstructionsforsecurityagainsttransientexecutionattacks AT nimishmathure verificationofserialisinginstructionsforsecurityagainsttransientexecutionattacks |