A Refinement-Based Approach to Spectre Invulnerability Verification

Several mitigations to thwart Spectre attacks have been proposed. However, design errors or trojans can be exploited to circumvent these mitigations. We have developed a highly-automated formal verification methodology that can detect if modern microprocessor designs are vulnerable to Spectre and it...

Full description

Bibliographic Details
Main Authors: Nimish Mathure, Sudarshan K. Srinivasan, Kushal K. Ponugoti
Format: Article
Language:English
Published: IEEE 2022-01-01
Series:IEEE Access
Subjects:
Online Access:https://ieeexplore.ieee.org/document/9846988/