Invulnerability invariants for software controlled speculation
Abstract Spectre class of transient execution security attacks on modern microprocessors rely on speculative execution. Software Controlled Speculation (SCS) was proposed as a microarchitecture‐level defense in the original Spectre paper and has also been adopted by ARM. The idea with SCS is to allo...
Saved in:
| Main Authors: | , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Wiley
2024-12-01
|
| Series: | Electronics Letters |
| Subjects: | |
| Online Access: | https://doi.org/10.1049/ell2.70108 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1846120987352891392 |
|---|---|
| author | Nimish Mathure Sudarshan K. Srinivasan Kushal K. Ponugoti |
| author_facet | Nimish Mathure Sudarshan K. Srinivasan Kushal K. Ponugoti |
| author_sort | Nimish Mathure |
| collection | DOAJ |
| description | Abstract Spectre class of transient execution security attacks on modern microprocessors rely on speculative execution. Software Controlled Speculation (SCS) was proposed as a microarchitecture‐level defense in the original Spectre paper and has also been adopted by ARM. The idea with SCS is to allow a mode in the microarchitecture, where instructions that read from memory are not allowed to execute speculatively. Errors or malicious fault‐injections in the implementation of SCS can still render the microarchitecture vulnerable to Spectre attacks. A formal verification method is proposed that can check the correctness of the implementation of SCS and detect any faults. The method has been demonstrated to be very efficient on two sets of benchmarks and provides accurate detection of implementation faults in SCS. |
| format | Article |
| id | doaj-art-e1ced21e17084b2e9a54a0570e5ed1c3 |
| institution | Kabale University |
| issn | 0013-5194 1350-911X |
| language | English |
| publishDate | 2024-12-01 |
| publisher | Wiley |
| record_format | Article |
| series | Electronics Letters |
| spelling | doaj-art-e1ced21e17084b2e9a54a0570e5ed1c32024-12-16T06:52:28ZengWileyElectronics Letters0013-51941350-911X2024-12-016023n/an/a10.1049/ell2.70108Invulnerability invariants for software controlled speculationNimish Mathure0Sudarshan K. Srinivasan1Kushal K. Ponugoti2Electrical 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 Spectre class of transient execution security attacks on modern microprocessors rely on speculative execution. Software Controlled Speculation (SCS) was proposed as a microarchitecture‐level defense in the original Spectre paper and has also been adopted by ARM. The idea with SCS is to allow a mode in the microarchitecture, where instructions that read from memory are not allowed to execute speculatively. Errors or malicious fault‐injections in the implementation of SCS can still render the microarchitecture vulnerable to Spectre attacks. A formal verification method is proposed that can check the correctness of the implementation of SCS and detect any faults. The method has been demonstrated to be very efficient on two sets of benchmarks and provides accurate detection of implementation faults in SCS.https://doi.org/10.1049/ell2.70108formal verificationsecurity of data |
| spellingShingle | Nimish Mathure Sudarshan K. Srinivasan Kushal K. Ponugoti Invulnerability invariants for software controlled speculation Electronics Letters formal verification security of data |
| title | Invulnerability invariants for software controlled speculation |
| title_full | Invulnerability invariants for software controlled speculation |
| title_fullStr | Invulnerability invariants for software controlled speculation |
| title_full_unstemmed | Invulnerability invariants for software controlled speculation |
| title_short | Invulnerability invariants for software controlled speculation |
| title_sort | invulnerability invariants for software controlled speculation |
| topic | formal verification security of data |
| url | https://doi.org/10.1049/ell2.70108 |
| work_keys_str_mv | AT nimishmathure invulnerabilityinvariantsforsoftwarecontrolledspeculation AT sudarshanksrinivasan invulnerabilityinvariantsforsoftwarecontrolledspeculation AT kushalkponugoti invulnerabilityinvariantsforsoftwarecontrolledspeculation |