arXiv · 2412.08769
Security Properties for Open-Source Hardware Designs
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.
Explore related subjects
Keep this discovery
Explore connections, maps & timelines
Jayden Rogers, Niyaz Shakeel, Divya Mankani, Samantha Espinosa, Cade Chabra, Kaki Ryan, Cynthia Sturton. 2024-12-11. Security Properties for Open-Source Hardware Designs. https://arxiv.org/abs/2412.08769
Cite the original work for its findings. Save a collection to share your selection of sources.