2024/12/11 by Jayden Rogers, Niyaz Shakeel, Rogers, Jayden +11
Computer Science · #Cloud Data Security Solutions #Cryptography and Security (cs.CR) #FOS: Computer and information sciences #Hardware Architecture (cs.AR) #Physical Unclonable Functions (PUFs) and Hardware Security #Security and Verification in Computing
paper · pdf · doi:10.48550/arxiv.2412.08769
openalex publication_date 2024/12/11 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
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.