Pith. sign in

REVIEW 3 major objections 4 minor 71 references

Security Properties for Open-Source Hardware Designs

T0 review · 3 major / 4 minor · reviewed 2026-08-11 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read This paper supplies open-source SystemVerilog assertions that catch known security bugs in four processor designs.

desk verdict Useful benchmark resource, but the 'well-vetted' claim is undercut by a likely false positive in Listing 4 and no golden-design check. read the letter →

arxiv 2412.08769 v2 pith:EH4ZNDK7 submitted 2024-12-11 cs.CR cs.AR

Jayden Rogers , Niyaz Shakeel , Divya Mankani , Samantha Espinosa , Cade Chabra , Kaki Ryan , Cynthia Sturton This is my paper · ORCID
classification cs.CRcs.AR
keywords propertiesSystemVerilogAssertionsregistertransferlevelverificationformalmethodshardwaresecurityopen-sourceCWE
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

Hardware-security verification research is slowed by a missing ingredient: published, machine-readable properties that say what secure behavior a design should have. This paper supplies that ingredient as a public benchmark: 122 SystemVerilog Assertions written against snapshotted versions of four commonly used open-source processor and SoC designs, with each assertion tied to the security flaw and CWE weakness class it addresses. The OR1200 assertion set detects all 31 known bugs inserted into that design, the PULPissimo set targets 31 known bugs with 20 assertions, and the two OpenPiton/CVA6 sets field 11 and 20 assertions for their 66 and 99 known bugs. A reproducibility case study on the PULPissimo design indicates that the same design and the same verification tool yield different bug detections when the properties differ, which is why the properties themselves need to be shared. A described methodology for writing such properties is meant to encourage other groups to publish theirs.

What carries the argument

The central object is the SystemVerilog Assertion (SVA), the industry-standard language for specifying hardware behavior as trace properties. The properties here are all safety properties: each one says that some undesirable state or finite sequence of states is never reached, and each is sampled at clock edges in a specific clock domain. The machine-readable assertion is paired with a static snapshot of the design it was written against, because signal names and cycle timing vary between design versions; the snapshot-plus-assertion pair is what makes a verification result reproducible. The verification engine searches for counterexamples to each assertion on the buggy design, so the assertion's job is to fire exactly when the known buggy behavior occurs.

What would settle it

Run the published assertions against a corrected version of one of the designs with the known bugs fixed; any assertion that still produces a counterexample is a false positive and is not a sound security specification. The OR1200 set is the easiest test because all 31 bugs are known and a corrected design could be constructed by reverting the 31 insertions.

Watch

Extended reading notes

Core claim

The paper's contribution is a reusable benchmark rather than a new theorem: for each of four widely used open-source processor or SoC designs, it provides a snapshotted buggy design plus a set of SystemVerilog Assertions that pinpoint known security bugs. The OR1200 benchmark contains 31 known bugs and 71 assertions that detect all of them; the PULPissimo benchmark has 20 assertions targeting 31 known bugs; the 2019 and 2021 OpenPiton/CVA6 benchmarks have 11 and 20 assertions targeting 66 and 99 bugs, respectively. Each assertion is tied to a CWE weakness class, and the authors verified with a commercial formal-verification tool that the assertions fire on the buggy designs. The paper also argues that the absence of shared properties is itself an obstacle: in a case study using the same PULPissimo design and the same tool as a prior study, different hand-written assertions produced different detection results, so the properties, not just the design and tool, are what make an evaluation reproducible.

Load-bearing premise

The benchmark's usefulness rests on the assumption that the assertions describe behavior a correct design should satisfy, not just behavior that happens to differ in these buggy snapshots; the paper does not check the assertions against a corrected, bug-free version of any design.

Editorial extensions

If this is right

  • A new formal-verification tool can be evaluated against a fixed target: run it on the snapshotted designs and compare its counterexamples with the published assertions and known bugs.
  • CWE tagging lets the community see which classes of security flaws are covered and which remain hard to capture, so benchmark coverage can grow by weakness category.
  • The reproducibility case study implies that prior published detection numbers are tied to the specific properties used; tool comparisons need a shared property set to be meaningful.
  • The stated methodology gives other groups a step-by-step recipe for writing and publishing properties, which the paper argues will make future verification results easier to compare.
  • Automated property generators, including LLM-based ones, gain a set of known-good assertions to use as a reference or seed set, which the paper identifies as a missing resource.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • If the assertions are sound, they could serve as regression checks on patched versions of these processors; that use is implicit in the benchmark design but not tested in the paper.
  • A natural extension would be to run the 71 OR1200 assertions against a corrected OR1200 with the 31 bugs reverted, to quantify false positives; the paper does not perform this check.
  • The paper's difficulty writing a property for one 2021 OpenPiton bug that it had captured in the 2019 design suggests a concrete challenge: target property-generation tools at exactly the bugs that resisted hand-written assertions.
  • The case study's result implies that, community-wide, reporting detection results without sharing properties is not enough to reproduce them; a requirement to publish properties would follow from the paper's argument, though the paper stops short of recommending it.
Share X Bluesky LinkedIn Reddit HN

Signed reviews

No signed human review yet.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

3 major / 4 minor

Summary. The paper addresses the lack of publicly available, formally specified security properties for open-source hardware designs. The authors provide SystemVerilog Assertions (SVA) for four buggy designs: OR1200 (71 properties), Hack@DAC 2018 PULPissimo (20), Hack@DAC 2019 OpenPiton/CVA6 (11), and Hack@DAC 2021 OpenPiton/CVA6 (20). They report that the properties detect all known bugs in each design using Cadence JasperGold, provide snapshotted designs in a public repository, map bugs to CWEs, and describe a manual property-writing methodology. The paper also presents a case study comparing their PULPissimo property results with those of HardFails, arguing that differing outcomes stem from unavailable properties, and concludes that open-sourcing properties improves reproducibility.

Significance. If the property sets are correct and reusable, this is a valuable community resource: it fills a genuine gap in the hardware security verification ecosystem, provides ground-truth benchmarks with known bugs, and gives the first substantial public SVA property corpus for these four widely used designs. The repository structure, the CWE tagging, and the attempt to document methodology and pitfalls are practical contributions that many groups can build on. The reproducibility case study is also useful as evidence that property availability materially affects reported verification results. The paper's main weakness is that property soundness is not established: there is no evaluation on a bug-free or corrected design, and at least one property shown in the paper appears to flag legal RISC-V behavior, which undermines the 'well-vetted' claim.

major comments (3)
  1. [Section 4, Listing 4] The assertion for Bug 3, shown in Listing 4, is not sound as a security property for a RISC-V core. It asserts that it is never the case that priv_lvl_n == PRIV_LVL_M and mstatus_n.mpp == PRIV_LVL_U. In the RISC-V privilege specification, when a trap is taken from U-mode to M-mode, the hardware sets mstatus.MPP to U and enters M-mode; this state is the architecturally correct post-trap state. A conforming core will therefore enter (M, MPP=U) on every user-mode trap, and this assertion would report a violation on correct behavior. If this property is faithfully represented in the repository, the benchmark will produce false positives on any correct RISC-V core, directly contradicting the paper's characterization of the properties as 'well-vetted'. The property must be qualified (for example, constrained to non-trap contexts or checked against the actual trap source) and revalidated.
  2. [Section 3.1, Step 5] The methodology explicitly acknowledges that 'the absence of a violation does not necessarily indicate the property is sound' for setting #1, yet the paper's main contribution is advertised as 'well-vetted properties'. There is no positive control: none of the four design snapshots was checked against a known-good or bug-corrected version to see whether the properties remain silent. Given the concrete false-positive risk in Listing 4, the paper needs to either provide such a validation for all shipped properties or temper the 'well-vetted' claim. A benchmark used by the community must not only detect known bugs but also avoid false alarms on correct designs, and the current evidence does not establish the latter.
  3. [Abstract and Section 1] The abstract's statement that the properties are 'successfully detecting all known bugs' is an existence claim about bug detection, but the paper implicitly also claims the properties express desired secure behavior (Section 3.1, setting #1). These are different claims, and the paper never separates them in the results. For example, some OR1200 properties are said to target 'behaviors related to the inserted bugs' while others are based on prior requirements; no distinction is drawn in the evaluation, and the reader cannot tell which properties are intended as general security specifications and which are bug-specific checkers. Since the central contribution is a reusable property set, this distinction is load-bearing and should be clarified and evaluated separately.
minor comments (4)
  1. [Section 3.1, paragraph 2] There is a typo: 'straighforward' should be 'straightforward'.
  2. [References] References [29] and [30] are both labeled 'Hack@DAC' with similar URLs but refer to different years; the citation in Section 3.2.3 ('2021 [30]') is correct, but the reference list would benefit from clearer year disambiguation to avoid reader confusion.
  3. [Table 1] The table would be easier to interpret if it included the total number of bugs found per CWE as a separate row or if the 'No. of Bugs Found' entries were annotated with the property identifiers from the repository, since the paper does not discuss which properties correspond to which bugs.
  4. [Section 4] The case study compares results with HardFails but does not provide the actual SVA properties used for each bug; while the full list is in the repository, a table in the appendix mapping bug IDs to property names would make the reproducibility argument more self-contained.

Circularity Check

0 steps flagged · score 2.0 of 10

No load-bearing circularity: the property set is an externally grounded benchmark; self-citations are minor and not the basis of the central claim.

full rationale

The paper's central contribution is a public set of SVA security properties for four buggy designs plus a methodology for writing them. There is no first-principles derivation that could be circular: the properties are hand-crafted from external bug descriptions, CWE mappings, and design RTL (Section 3.1 steps 1-5; Sections 3.2.1-3.2.3). The statement that 71 properties 'successfully detect all known bugs' is a report of property-bug matching for a benchmark, not a prediction of unknown bugs; the properties were written to catch those same known bugs, so the detection is a sanity check rather than independent validation. That self-matching is inherent to benchmark construction and is not presented as a derived result. The paper cites prior work by its own authors (e.g., [32], [68], [69] for OR1200 property inspiration and bug sources), but these are stated as inspiration/source material, and the actual assertions, snapshots, and bug mappings are new artifacts in the repository. No uniqueness theorem or ansatz is imported from the authors' prior work, and no known result is merely renamed. The paper explicitly acknowledges the soundness limitation in Section 3.1 step 5: 'the absence of a violation does not necessarily indicate the property is sound.' The reviewer concern that Listing 4 forbids a legal RISC-V trap state (M-mode with mstatus.MPP=U) is a potential false-positive/soundness defect, not a circularity step; if confirmed against the snapshotted RTL, it would weaken the 'well-vetted' claim but does not make the derivation equivalent to its inputs. Overall, the self-citations are minor and non-load-bearing, so the appropriate score is low.

Assumptions & free parameters 0 free parameters · 3 assumptions · 0 invented entities

The central claims rest on the fidelity of the known-bug descriptions, the soundness of the properties on correct designs, and the trustworthiness of JasperGold. No free parameters or invented entities are introduced. The main unvalidated assumption is the absence of false positives.

assumptions (3)
  • domain assumption The 31 known bugs in OR1200 and the 66 and 99 bugs in the 2019 and 2021 OpenPiton designs, as described in the cited literature, are correctly identified and faithfully represented in the snapshotted designs.
    The paper relies on prior bug descriptions (e.g., [15], [27], [28], [31]) without independently verifying the ground truth; Section 3.2.2 and 3.2.3.
  • domain assumption The properties, when satisfied, correspond to secure behavior and are not violated on a correct design (no false positives).
    The paper only verifies that properties catch known bugs and does not test against a golden or bug-free design; Section 3.1 step 5.
  • domain assumption JasperGold formal verification is reliable for the reported checks.
    The paper uses JasperGold FPV to establish that properties detect bugs; this is an industry-standard tool, but the authors do not discuss tool configuration or potential tool errors.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Security Properties for Open-Source Hardware Designs." pith.science (2026). https://pith.science/paper/EH4ZNDK7

@misc{pith2026241208769,
  author       = {Pith},
  title        = {Pith review of: Security Properties for Open-Source Hardware Designs},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/EH4ZNDK7}},
  note         = {Machine review of arXiv:2412.08769}
}
read the original 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.

Figures

Figures reproduced from arXiv: 2412.08769 by the authors.

Figure 1
Figure 1. In the hardware verification community there is no [PITH_FULL_IMAGE:figures/full_fig_p001_1.png] view at source ↗

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

71 extracted references · 64 canonical work pages

  1. [1]

    IEEE Standard for SystemVerilog–Unified Hardware Design, Specification, and Verification Language

    2018. IEEE Standard for SystemVerilog–Unified Hardware Design, Specification, and Verification Language. IEEE Std 1800-2017 (Revision of IEEE Std 1800-2012) (2018), 1–1315

    work page 2018

  2. [2]

    Ahmad, W

    B. Ahmad, W. Liu, L. Collini, H. Pearce, J. M. Fung, J. Valamehr, M. Bidmeshki, P. Sapiecha, S. Brown, K. Chakrabarty, R. Karri, and B. Tan. 2022. Don’t CWEAT It: Toward CWE Analysis Techniques in Early Stages of Hardware Design. In ICCAD (ICCAD ’22) . ACM

    work page 2022

  3. [3]

    A. L. D. Antón, J. Müller, M. R. Fadiheh, D. Stoffel, and W. Kunz. 2023. Fault Attacks on Access Control in Processors: Threat, Formal Analysis and Microar- chitectural Mitigation. IEEE Access (2023)

    work page 2023

  4. [4]

    Ardeshiricham, W

    A. Ardeshiricham, W. Hu, J. Marxen, and R. Kastner. 2017. Register transfer level information flow tracking for provably secure hardware design. In Design, Automation & Test in Europe Conference & Exhibition (DATE), 2017 . 1691–1696

    work page 2017

  5. [5]

    Balkind, M

    J. Balkind, M. McKeown, Y. Fu, T. Nguyen, Y. Zhou, A. Lavrov, M. Shahrad, A. Fuchs, S. Payne, X. Liang, M. Matl, and D. Wentzlaff. 2016. OpenPiton: An Open Source Manycore Research Framework. In Proceedings of the Twenty-First International Conference on Architectural Support for Programming Languages and Operating Systems (Atlanta, Georgia, USA) (ASPLOS ...

    work page 2016

  6. [6]

    Bilzor, T

    M. Bilzor, T. Huffmire, C. Irvine, and T. Levin. 2011. Security Checkers: Detecting processor malicious inclusions at runtime. In HOST. https://doi.org/10.1109/ HST.2011.5954992

    work page arXiv 2011

  7. [7]

    Bugzilla. [n. d.]. Bugzilla. https://www.bugzilla.org/

    work page

  8. [8]

    Canakci, L

    S. Canakci, L. Delshadtehrani, F. Eris, M. B. Taylor, M. Egele, and A. Joshi. 2021. Directfuzz: Automated test generation for rtl designs using directed graybox fuzzing. In DAC. IEEE, 529–534

    work page 2021

Show all 71 references
  1. [9]

    Canakci, C

    S. Canakci, C. Rajapaksha, L. Delshadtehrani, A. Nataraja, M. B. Taylor, M. Egele, and A. Joshi. 2023. ProcessorFuzz: Processor Fuzzing with Control and Status Registers Guidance. In HOST. IEEE, 1–12

    2023

  2. [10]

    C. Chen, V. Gohil, R. Kande, A-R. Sadeghi, and J. Rajendran. 2023. PSOFuzz: Fuzzing Processors with Particle Swarm Optimization. In ICCAD. IEEE, 1–9

    2023

  3. [11]

    Chen Chen, Rahul Kande, Pouya Mahmoody, Ahmad-Reza Sadeghi, and JV Rajendran. 2022. Trusting the trust anchor: towards detecting cross-layer vul- nerabilities with hardware fuzzing. In DAC. 1379–1383

    2022

  4. [12]

    C. Chen, R. Kande, N. Nyugen, F. Andersen, A. Tyagi, A-R. Sadeghi, and J. Ra- jendran. 2023. HyPFuzz: Formal-Assisted Processor Fuzzing. arXiv preprint arXiv:2304.02485 (2023)

    2023 arXiv

  5. [13]

    Cycuity. [n. d.]. https://cycuity.com/ Security Properties for Open-Source Hardware Designs

  6. [14]

    Cycuity. [n. d.]. Radix Coverage for Hardware Common Weakness Enumera- tion (CWE) Guide. https://cycuity.com/type/white_paper/radix-coverage-for- hardware-common-weakness-enumeration-cwe-guide/

  7. [15]

    Dessouky, D

    G. Dessouky, D. Gens, P. Haney, G. Persyn, A. Kanuparthi, H. Khattri, J. M. Fung, A.-R. Sadeghi, and J. Rajendran. 2019. HardFails: Insights into Software- Exploitable Hardware Bugs. In USENIX Security. USENIX Association, Santa Clara, CA, 213–230

    2019

  8. [16]

    Deutschbein

    C. Deutschbein. 2021. Mining Secure Behavior of Hardware Designs . Ph. D. Dissertation. The University of North Carolina at Chapel Hill

    2021

  9. [17]

    Deutschbein, A

    C. Deutschbein, A. Meza, F. Restuccia, R. Kastner, and C. Sturton. 2021. Isadora: Automated Information Flow Property Generation for Hardware Designs. In ASHES. ACM

    2021

  10. [18]

    Deutschbein and C

    C. Deutschbein and C. Sturton. 2020. Evaluating Security Specification Mining for a CISC Architecture. In HOST. IEEE

    2020

  11. [19]

    N. F. Dipu, A. Ayalasomayajula, M. Tehranipoor, and F. Farahmandi. 2023. AGILE: Automated Assertion Generation to Detect Information Leakage Vulnerabilities. IEEE Transactions on Information Forensics and Security (2023)

    2023

  12. [20]

    W. Fang, M. Li, M. Li, Z. Yan, S. Liu, Z. Xie, and H. Zhang. 2024. AssertLLM: Generating and Evaluating Hardware Verification Assertions from Design Speci- fications via Multi-LLMs. arXiv:2402.00386 [cs.AR]

    2024

  13. [21]

    Fang and H

    W. Fang and H. Zhang. 2023. WASIM: A word-level abstract symbolic simulation framework for hardware formal verification. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems . Springer, 11–18

    2023

  14. [22]

    Farzana, F

    N. Farzana, F. Farahmandi, and M. Tehranipoor. 2021. SoC Security Properties and Rules. IACR Cryptology ePrint Archive (2021)

    2021

  15. [23]

    Farzana, F

    N. Farzana, F. Rahman, M. Tehranipoor, and F. Farahmandi. 2019. SoC Security Verification using Property Checking. In ITC. 1–10

    2019

  16. [24]

    Gogri, P

    S. Gogri, P. Joshi, P. Vurikiti, N. Fern, M. Quinn, and J. Valamehr. 2021. Texas A&M Hackin’ Aggies’ Security Verification Strategies for the 2019 Hack@DAC Competition. IEEE Design & Test 38, 1 (2021), 30–38

    2021

  17. [25]

    Gohil, R

    V. Gohil, R. Kande, C. Chen, A-R. Sadeghi, and J. Rajendran. 2023. MABFuzz: Multi- Armed Bandit Algorithms for Fuzzing Processors.arXiv preprint arXiv:2311.14594 (2023)

    2023 arXiv

  18. [26]

    Hack@DAC. [n. d.]. https://www.dac.com/Conference/HackDAC

  19. [27]

    Hack@DAC 2018 Phase 2 Buggy SoC. [n. d.]. https://github.com/hackdac/ hackdac_2018_beta

    2018

  20. [28]

    Hack@DAC 2019. [n. d.]. https://hackthesilicon.com/dac19-setup/

    2019

  21. [29]

    Hack@DAC 2019 Alpha Stage SoC. [n. d.]. https://github.com/HACK-EVENT/ hackatdac19

    2019

  22. [30]

    Hack@DAC 2021 Alpha Stage SoC. [n. d.]. https://github.com/HACK-EVENT/ hackatdac21

    2021

  23. [31]

    Hack@DAC 2021 SoC. [n. d.]. https://github.com/HACK-EVENT/hackatdac21

    2021

  24. [32]

    Hicks, C

    M. Hicks, C. Sturton, S. T. King, and J. M. Smith. 2015. Specs: A lightweight runtime mechanism for protecting software from security-critical processor bugs. In ASPLOS. 517–529

    2015

  25. [33]

    M. M. Hossain, N. F. Dipu, K. Z. Azar, F. Rahman, F. Farahmandi, and M. Tehra- nipoor. 2023. TaintFuzzer: SoC Security Verification using Taint Inference- enabled Fuzzing. In ICCAD. IEEE, 1–9

    2023

  26. [34]

    M. M. Hossain, A. Vafaei, K. Z. Azar, F. Rahman, F. Farahmandi, and M. Tehra- nipoor. 2023. Socfuzzer: Soc vulnerability detection using cost function enabled fuzz testing. In DATE. IEEE, 1–6

    2023

  27. [35]

    W. Hu, A. Ardeshiricham, M. S. Gobulukoglu, X. Wang, and R. Kastner. 2018. Property Specific Information Flow Analysis for Hardware Security Verification. In ICCAD. 1–8

    2018

  28. [36]

    W. Hu, A. Ardeshiricham, and R. Kastner. 2021. Hardware information flow tracking. CSUR 54, 4 (2021), 1–39

    2021

  29. [37]

    Kande, H

    R. Kande, H. Pearce, B. Tan, B. Dolan-Gavitt, S. Thakur, R. Karri, and J. Rajen- dran. 2023. LLM-assisted Generation of Hardware Assertions. arXiv preprint arXiv:2306.14027 (2023)

    2023 arXiv

  30. [38]

    Kastner, F

    R. Kastner, F. Restuccia, A. Meza, S. Ray, J. Fung, and C. Sturton. 2022. Automating hardware security property generation. In DAC. 1384–1387

    2022

  31. [39]

    Lyu and P

    Y. Lyu and P. Mishra. 2020. Automated test generation for activation of assertions in RTL models. In ASP-DAC. IEEE, 223–228

    2020

  32. [40]

    X. Meng. 2023. Ensuring Hardware Robustness via Security Verification . Ph. D. Dissertation

    2023

  33. [41]

    X. Meng, S. Kundu, A. K. Kanuparthi, and K. Basu. 2021. Rtl-contest: Con- colic testing on rtl for detecting security vulnerabilities. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems 41, 3 (2021), 466–477

    2021

  34. [42]

    X. Meng, A. Srivastava, A. Arunachalam, A. Ray, P. H. Silva, R. Psiakis, Y. Makris, and K. Basu. 2023. Unlocking hardware security assurance: The potential of llms. arXiv preprint arXiv:2308.11042 (2023)

    2023 arXiv

  35. [43]

    A. Meza, F. Restuccia, J. Oberg, D. Rizzo, and R. Kastner. 2023. Security Verification of the OpenTitan Hardware Root of Trust. IEEE S&P 21, 3 (2023), 27–36

    2023

  36. [44]

    MITRE. [n. d.]. Common Weakness Enumeration. https://cwe.mitre.org/

  37. [45]

    Müller, M

    J. Müller, M. R. Fadiheh, A. L. D. Antón, T. Eisenbarth, D. Stoffel, and W. Kunz

  38. [46]

    OpenCores. [n. d.]. OpenCores. https://opencores.org/

  39. [47]

    OR1200: OpenRISC 1200 Implementation. [n. d.]. https://github.com/openrisc/ or1200

  40. [48]

    Paria, A

    S. Paria, A. Dasgupta, and S. Bhunia. 2023. DIVAS: An LLM-based End-to-End Framework for SoC Security Analysis and Policy-based Protection.arXiv preprint arXiv:2308.06932 (2023)

    2023 arXiv

  41. [49]

    Patterson

    D. Patterson. 2012. For better or worse, benchmarks shape a field: technical perspective. Commun. ACM 55, 7 (July 2012), 104

    2012

  42. [50]

    M. Qin, J. Li, J. Yan, Z. Hao, W. Hu, and B. Liu. 2024. HT-PGFV: Security-Aware Hardware Trojan Security Property Generation and Formal Security Verification Scheme. Electronics 13, 21 (2024)

    2024

  43. [51]

    S. R. Rajendran, N. F. Dipu, S. Tarek, H. M. Kamali, F. Farahmandi, and M. Tehra- nipoor. 2024. Exploring the Abyss? Unveiling Systems-on-Chip Hardware Vul- nerabilities beneath Software. IEEE Transactions on Information Forensics and Security (2024)

    2024

  44. [52]

    S. R. Rajendran, S. Tarek, B. M. Hicks, H. M. Kamali, F. Farahmandi, and M. Tehranipoor. 2023. HUnTer: Hardware Underneath Trigger for Exploiting SoC- level Vulnerabilities. In DATE. IEEE, 1–6

    2023

  45. [53]

    Restuccia, A

    F. Restuccia, A. Meza, and R. Kastner. 2021. AKER: A Design and Verification Framework for Safe andSecure SoC Access Control. arXiv:2106.13263 [cs.CR]

    2021 arXiv

  46. [54]

    Ryan and C

    K. Ryan and C. Sturton. 2023. Sylvia: Countering the Path Explosion Problem in the Symbolic Execution of Hardware Designs. In FMCAD. IEEE, 110–121

    2023

  47. [55]

    Sadeghi, J

    A.-R. Sadeghi, J. Rajendran, and R. Kande. 2021. Organizing The World’s Largest Hardware Security Competition: Challenges, Opportunities, and Lessons Learned (GLSVLSI ’21) . Association for Computing Machinery, New York, NY, USA, 95–100

    2021

  48. [56]

    P. D. Schiavone, D. Rossi, A. Pullini, A. Di Mauro, F. Conti, and L. Benini. 2018. Quentin: an Ultra-Low-Power PULPissimo SoC in 22nm FDX. In S3S. 1–3. https: //doi.org/10.1109/S3S.2018.8640145

    2018

  49. [57]

    SoC Vulnerability Database. [n. d.]. http://cad4security.org/index.php/riscv- vulnerability-details/

  50. [58]

    B. Solem. 2023. Applying Unique Program Execution Checking in the development flow of industrial IoT devices to prevent vulnerabilities for side-channel attacks . Master’s thesis. NTNU

    2023

  51. [59]

    F. Solt, B. Gras, and K. Razavi. 2022. {CellIFT}: Leveraging Cells for Scalable and Precise Dynamic Information Flow Tracking in{RTL}. In USENIX Security

    2022

  52. [60]

    Sugiyama, R

    Y. Sugiyama, R. Matsuo, and R. Shioya. 2023. SurgeFuzz: Surge-Aware Directed Fuzzing for CPU Designs. In ICCAD. IEEE, 1–9

    2023

  53. [61]

    Tarek, H

    S. Tarek, H. Al Shaikh, S. R. Rajendran, and F. Farahmandi. 2023. Benchmarking of SOC-level hardware vulnerabilities: A complete walkthrough. In ISVLSI. IEEE, 1–6

    2023

  54. [62]

    Trippel, K

    T. Trippel, K. G. Shin, A. Chernyakhovsky, G. Kelly, D. Rizzo, and M. Hicks. 2022. Fuzzing hardware like software. In USENIX Security 22. 3237–3254

    2022

  55. [63]

    Trust-Hub. [n. d.]. https://www.trust-hub.org

  56. [64]

    Tyagi, A

    A. Tyagi, A. Crump, A-R. Sadeghi, G. Persyn, J. Rajendran, P. Jauernig, and R. Kande. 2022. Thehuzz: Instruction fuzzing of processors using golden- reference models for finding software-exploitable vulnerabilities. arXiv preprint arXiv:2201.09941 (2022)

    2022 arXiv

  57. [65]

    J. Xu, Y. Liu, S. He, H. Lin, Y. Zhou, and C. Wang. 2023. {MorFuzz}: Fuzzing Processor via Runtime Instruction Morphing enhanced Synchronizable Co- simulation. In USENIX Security 23. 1307–1324

    2023

  58. [66]

    Zaruba and L

    F. Zaruba and L. Benini. 2019. The Cost of Application-Class Processing: Energy and Performance Analysis of a Linux-Ready 1.7-GHz 64-Bit RISC-V Core in 22-nm FDSOI Technology. VLSI 27, 11 (Nov 2019), 2629–2640

    2019

  59. [67]

    Zhang, C

    R. Zhang, C. Deutschbein, P. Huang, and C. Sturton. 2018. End-to-end automated exploit generation for validating the security of processor designs. In MICRO. IEEE, 815–827

    2018

  60. [68]

    Zhang, N

    R. Zhang, N. Stanley, C. Griggs, A. Chi, and C. Sturton. 2017. Identifying Security Critical Properties for the Dynamic Verification of a Processor. InASPLOS (Xi’an, China) (ASPLOS ’17). ACM, New York, NY, USA, 541–554

    2017

  61. [69]

    Zhang and C

    R. Zhang and C. Sturton. 2020. Transys: Leveraging Common Security Properties Across Hardware Designs. In IEEE S&P. IEEE

    2020

  62. [70]

    Zhang, G

    Z. Zhang, G. Chadwick, H. McNally, Y. Zhao, and R. Mullins. 2023. LLM4DV: Using Large Language Models for Hardware Test Stimuli Genera- tion. arXiv:2310.04535 [cs.LG]

    2023 arXiv

  63. [2021]

    A formal approach to confidentiality verification in SoCs at the register transfer level. In DAC. IEEE, 991–996

Pith tools

Reviewed August 11, 2026 · model on record in the stance chip above.