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.

翻译：硬件安全领域依赖已知漏洞数据库与开源设计来开发形式化验证方法，以识别硬件安全缺陷。尽管存在大量开源设计与验证工具，但针对这些缺陷的开源属性库仍存在空白，这导致先前工作难以复现并阻碍了研究进展。本文旨在填补这一空白。我们为四个常见设计提供了SystemVerilog断言：OR1200、Hack@DAC 2018存在缺陷的PULPissimo SoC、Hack@DAC 2019的CVA6以及Hack@DAC 2021存在缺陷的OpenPiton SoC。这些属性按设计模块进行组织，并通过安全缺陷详情及关联的通用缺陷枚举（CWE）进行标记。为促进更多属性报告，我们详细阐述了构建属性时采用的方法论。