BlueVeri: Formal Security Verification for Bluespec Processor Designs

There are numerous hardware security defense mechanisms designed to mitigate sidechannel attacks. However, ensuring that a defense can comprehensively protect against an entire class of attacks, while avoiding the introduction of new vulnerabilities that could lead to additional attack surfaces, remains a significant challenge. Although researchers have attempted to apply formal verification techniques to hardware security, these efforts have been hindered by scalability issues. In this paper, we introduce BlueVeri, a systematic and automatable approach for formally verifying the security of a Bluespec processor against speculative execution attacks. BlueVeri leverages the high-level information provided by Bluespec’s guarded atomic actions, simplifying and accelerating the verification process. We evaluate BlueVeri on out-of-order processors implemented in Bluespec, demonstrating that our approach substantially enhances verification scalability and is capable of proving the security properties of a minimal out-of-order processor within one hour.

Name thesis:degree_name

Master

Department dc:contributor.department

Massachusetts Institute of Technology. Department of Electrical Engineering and Computer Science

Grantor dc:publisher

Massachusetts Institute of Technology

Year dc:date.issued

2025

Author dc:creator

• Wang, Shih-Yu

Advisor dc:contributor.advisor

• Yan, Mengjia

Statement dc:rights

• In Copyright - Educational Use Permitted
• Copyright retained by author(s)

Licence dc:rights.uri

• https://rightsstatements.org/page/InC-EDU/1.0/

Handle dc:identifier.uri

https://hdl.handle.net/1721.1/162936

OAI identifier oai:identifier

oai:dspace.mit.edu:1721.1/162936