Formal Verification for Secure Processors: A Guide for Computer Architects

Mengjia Yan; Thomas Bourgeat; Sharad Malik

doi:10.1109/MC.2024.3434848

Formal Verification for Secure Processors: A Guide for Computer Architects

Mengjia Yan, Thomas Bourgeat, Sharad Malik

Research output: Contribution to specialist publication › Article

Abstract

As computer architects continually push the limits of microarchitectural performance optimizations, securing hardware against speculative execution attacks feels like a Sisyphean task. This article explores the critical role computer architects can play in advancing hardware security through formal verification.

Original language	English (US)
Pages	138-143
Number of pages	6
Volume	57
No	10
Specialist publication	Computer
DOIs	https://doi.org/10.1109/MC.2024.3434848
State	Published - 2024
Externally published	Yes

All Science Journal Classification (ASJC) codes

General Computer Science

Access to Document

10.1109/MC.2024.3434848

Cite this

@misc{03d5ec33e18143aa9456aa2cd5d13104,

title = "Formal Verification for Secure Processors: A Guide for Computer Architects",

abstract = "As computer architects continually push the limits of microarchitectural performance optimizations, securing hardware against speculative execution attacks feels like a Sisyphean task. This article explores the critical role computer architects can play in advancing hardware security through formal verification.",

author = "Mengjia Yan and Thomas Bourgeat and Sharad Malik",

note = "Publisher Copyright: {\textcopyright} 1970-2012 IEEE.",

year = "2024",

doi = "10.1109/MC.2024.3434848",

language = "English (US)",

volume = "57",

pages = "138--143",

journal = "Computer",

issn = "0018-9162",

publisher = "IEEE Computer Society",

}

TY - GEN

T1 - Formal Verification for Secure Processors

T2 - A Guide for Computer Architects

AU - Yan, Mengjia

AU - Bourgeat, Thomas

AU - Malik, Sharad

PY - 2024

Y1 - 2024

N2 - As computer architects continually push the limits of microarchitectural performance optimizations, securing hardware against speculative execution attacks feels like a Sisyphean task. This article explores the critical role computer architects can play in advancing hardware security through formal verification.

AB - As computer architects continually push the limits of microarchitectural performance optimizations, securing hardware against speculative execution attacks feels like a Sisyphean task. This article explores the critical role computer architects can play in advancing hardware security through formal verification.

UR - http://www.scopus.com/inward/record.url?scp=85206438194&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=85206438194&partnerID=8YFLogxK

U2 - 10.1109/MC.2024.3434848

DO - 10.1109/MC.2024.3434848

M3 - Article

AN - SCOPUS:85206438194

SN - 0018-9162

VL - 57

SP - 138

EP - 143

JO - Computer

JF - Computer

ER -

Formal Verification for Secure Processors: A Guide for Computer Architects

Abstract

All Science Journal Classification (ASJC) codes

Access to Document

Other files and links

Fingerprint

Cite this