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!
|
| Summary: | 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. |
|---|---|
| ISSN: | 0013-5194 1350-911X |