Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Security Properties for Open-Source Hardware Designs

Jayden Rogers, Niyaz Shakeel, Divya Mankani, Samantha Espinosa, Cade Chabra, Kaki Ryan, Cynthia Sturton

TL;DR

The paper addresses the lack of open-source security properties for hardware designs and proposes four sets of SystemVerilog Assertions (SVA) targeting buggy designs OR1200, PULPissimo, and CVA6/OpenPiton (2019 and 2021). It details a replicable property-writing methodology and provides a public benchmark repository with 71, 20, 11, and 20 properties, each linked to corresponding CWEs and design snapshots, verified using JasperGold FPV. By including case studies on reproducibility, the work demonstrates how open properties improve comparability and repeatability across verification tools and research groups. Overall, it offers a practical open-source resource and process to accelerate evaluation of formal verification methods in hardware security and invites community collaboration.

Abstract

The hardware security community relies on databases of known vulnerabilities and open-source designs to develop formal verification methods for identifying hardware security flaws. While there are plenty of open-source designs and verification tools, there is a gap in open-source properties addressing these flaws, making it difficult to reproduce prior work and slowing research. This paper aims to bridge that gap. We provide SystemVerilog Assertions for four common designs: OR1200, Hack@DAC 2018's buggy PULPissimo SoC, Hack@DAC 2019's CVA6, and Hack@DAC 2021's buggy OpenPiton SoCs. The properties are organized by design and tagged with details about the security flaws and the implicated CWE. To encourage more property reporting, we describe the methodology we use when crafting properties.

Security Properties for Open-Source Hardware Designs

TL;DR

The paper addresses the lack of open-source security properties for hardware designs and proposes four sets of SystemVerilog Assertions (SVA) targeting buggy designs OR1200, PULPissimo, and CVA6/OpenPiton (2019 and 2021). It details a replicable property-writing methodology and provides a public benchmark repository with 71, 20, 11, and 20 properties, each linked to corresponding CWEs and design snapshots, verified using JasperGold FPV. By including case studies on reproducibility, the work demonstrates how open properties improve comparability and repeatability across verification tools and research groups. Overall, it offers a practical open-source resource and process to accelerate evaluation of formal verification methods in hardware security and invites community collaboration.

Abstract

The hardware security community relies on databases of known vulnerabilities and open-source designs to develop formal verification methods for identifying hardware security flaws. While there are plenty of open-source designs and verification tools, there is a gap in open-source properties addressing these flaws, making it difficult to reproduce prior work and slowing research. This paper aims to bridge that gap. We provide SystemVerilog Assertions for four common designs: OR1200, Hack@DAC 2018's buggy PULPissimo SoC, Hack@DAC 2019's CVA6, and Hack@DAC 2021's buggy OpenPiton SoCs. The properties are organized by design and tagged with details about the security flaws and the implicated CWE. To encourage more property reporting, we describe the methodology we use when crafting properties.

Paper Structure

This paper contains 14 sections, 1 figure, 1 table.

Table of Contents

  1. Introduction
  2. Background
  3. Scope
  4. Open-Source Resources
  5. Related Work
  6. Property Development
  7. Methodology
  8. Designs Studied
  9. OR1200
  10. Hack@DAC 2018
  11. Hack@DAC 2019 and 2021
  12. Property Examples
  13. Case Study: Examining the role properties play in reproducibility
  14. Conclusion

Figures (1)

  • Figure 1: In the hardware verification community there is no shortage of open-source designs or verification tools, but the verification properties still remain scarce, hard to find, and hard to write. This work aims to bridge that gap through both the contribution of an open-source database of properties, a methodology for property writing , and a call for authors to start providing the properties they use in their work.