Pith. sign in

REVIEW 3 major objections 5 minor 29 references

Translating Common Security Assertions Across Processor Designs: A RISC-V Case Study

T0 review · 3 major / 5 minor · reviewed 2026-08-07 · deepseek-v4-flash

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

Pith's one-line read Translated security assertions catch all 33 LLM-made Trojans across RISC-V cores.

desk verdict The 100% Trojan detection is circular, but the NS31A-to-Ibex assertion translation workflow is a documented, reproducible artifact that could be salvaged with independent validation. read the letter →

arxiv 2502.10194 v1 pith:TDYHMU6C submitted 2025-02-14 cs.CR cs.AR

Sharjeel Imtiaz , Uljana Reinsalu , Tara Ghasempouri This is my paper · ORCID
classification cs.CRcs.AR
keywords securityassertionsassertiontranslationRISC-VhardwareTrojandetectionSystemVerilogprocessorverificationLLM-generatedTrojanssignalmapping
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

This paper asks whether security assertions, which are expensive to write by hand, can be carried over from one processor design to another by translation. The authors translate a set of assertions from the NS31A RISC-V core into the Ibex RISC-V core for five security-critical modules, and report that every assertion ports cleanly. To test whether the translated checks actually enforce security, they generate hardware Trojans with a large language model, inject them into the target core, and find that all 33 Trojans are caught in simulation. If the result holds, a security property written once for one processor could be adapted to another without rewriting it from scratch, reducing the time and expertise needed for processor security verification.

What carries the argument

The load-bearing object is the SystemVerilog security assertion, in the form assert property (antecedent |=> consequent), with temporal operators ##N (wait N cycles) and $past (value at an earlier cycle) used to express ordering. Carrying the argument is a five-stage signal-linking pipeline: identify which signals from the original assertion exist in the target RTL; handle direct signal mappings; trace multi-layer indirect signal dependencies; drop signals or whole assertions that have no counterpart; and generate test cases to confirm the translated assertion fires. The argument rests on that pipeline preserving the assertion's logical condition even when signal names and internal logic differ between the two processors.

What would settle it

Take the same Ibex RTL and inject hardware Trojans that were created without access to the translated assertions, for example Trojans from a public hardware-Trojan benchmark or crafted by a designer who is deliberately trying to evade the asserted properties, and rerun the simulation testbench; if any such Trojan escapes detection, the 100% claim is limited to the paper's Trojan-generation setup.

Watch

Extended reading notes

Core claim

The paper's central claim is that security-assertion translation across RISC-V processors is both feasible and security-effective: the same security properties, expressed as SystemVerilog assertions, can be ported from NS31A to Ibex with 100% translation success across the PMP, CSR, DO, ETI, and CF modules, and the ported assertions subsequently detect every one of the 33 hardware Trojans generated for this study. The authors interpret the 100% detection rate as demonstrating the reliability of translated assertions in detecting security breaches, and they support the result with two metrics: a Trojan Power Index that quantifies how hard each Trojan is to trigger, and a Trojan Detection Efficiency Ratio that scores assertion coverage.

Load-bearing premise

The validation would collapse if the hardware Trojans generated by the language model after being told to target the translated assertions are not representative of real-world hardware Trojans, because then the 100% detection rate would be a consequence of how the Trojans were made rather than of the assertions' strength.

Editorial extensions

If this is right

  • Security assertions do not have to be written from scratch for each new processor; a defined signal-mapping procedure can carry them across designs.
  • Translated assertions keep their detecting power in the target design, at least for the five modules studied, since all 33 injected Trojans were caught.
  • The TPI and TDER metrics give designers a quantitative way to compare Trojan difficulty and assertion coverage across different processor designs.
  • Because the dependency-tracing stages are not RISC-V-specific, the translation methodology should apply to other RISC-V cores and possibly to other processor families.
  • Reusing assertions this way reduces the time and cost of assertion-based security verification compared to manual assertion development.

Reading between the lines

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

  • An implication not drawn in the paper: the 100% detection rate should be read as applying to the paper's Trojan-generation setup; Trojans created without knowledge of the assertions, or those that trigger on boundary conditions outside the asserted signals, would be a sterner test and would likely lower the rate.
  • The signal-dependency tracing that makes assertion translation work could also be used to port functional coverage properties or formal constraints between RTL designs, turning single-design verification artifacts into reusable ones.
  • Because the LLM was instructed to leave module interfaces unchanged and to embed Trojans only in the asserted regions, the experiment does not yet cover Trojans that modify top-level behavior or communicate covertly across modules; that is a natural next target for the same methodology.
  • The TPI metric could be inverted into a design-time tool: compute the triggering probability of candidate malicious conditions before fabrication and rank assertion coverage by the highest-TPI Trojans that remain undetected.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

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

Referee Report

3 major / 5 minor

Summary. The paper proposes a methodology for translating security assertions from one RISC-V processor (NS31A) to another (Ibex) across five modules (PMP, CSR, DO, ETI, CF). The authors report 100% assertion translation success and 100% detection of 33 hardware Trojans generated by ChatGPT, and introduce two metrics, TPI (Trojan Power Index) and TDER (Trojan Detection Efficiency Ratio). The paper argues that this demonstrates the reliability of translated assertions in detecting security breaches, reducing the cost of manual assertion development.

Significance. The problem addressed—reusing security assertions across processor designs—is relevant and timely, and the proposed translation workflow could be a useful practical tool. However, the paper's central security claim rests entirely on an experimental design in which the Trojans are generated from prompts that explicitly target the translated assertions and whose test cases are also generated to activate those same Trojans. As a result, the reported 100% detection rate is a tautology of the generation protocol, not evidence that the assertions detect realistic hardware Trojans. The translation fidelity is also self-assessed with no independent oracle. If the validation were redesigned with independent Trojan benchmarks and a control condition, the underlying translation methodology might be salvageable, but as submitted the main claim is unsupported.

major comments (3)
  1. [Section III-B, Table I, Eq. (2)] The 100% Trojan detection rate is an artifact of the generation protocol. The Task section of the prompt explicitly instructs ChatGPT to "generate Trojans according to the translated assertions" and to focus "on areas where these assertions are applied," and the Output Required section asks for test cases designed to activate those Trojans. Consequently, each of the 33 Trojans is constructed to trigger exactly the conditions monitored by the translated assertions. The TDER metric in Eq. (2) therefore measures whether the assertions fire on the conditions they were designed to flag, which is a positive-control test, not a test of detection of realistic hardware Trojans. The Abstract and Section V overstate this result as demonstrating "their reliability in detecting security breaches."
  2. [Section III-A, Step 5 (Test Case generation), Table I] The assertion translation success is assessed only with hand-written test cases generated from the translated assertions themselves. There is no independent oracle—such as formal equivalence checking of the translated property against the original, or evaluation against a third-party assertion suite—to confirm that the translated assertions preserve the intended security semantics. A translation that weakens, narrows, or alters a security condition could still pass the authors' own test cases. The 100% Translation % in Table I thus reflects internal consistency of the authors' test cases rather than translation fidelity to the original security properties.
  3. [Section III-B and Table I] The evaluation lacks any control condition or independent Trojan benchmark. The paper reports no Trojans from an established source such as Trust-Hub, no Trojans generated under a prompt that forbids the LLM from using assertion-relevant signals or that targets modules outside the assertion-covered areas, and no negative-control prompt. Without such baselines, the Trojan Detection % column cannot distinguish a genuinely protective assertion set from assertions that merely encode the prompt's own targeting decisions. Adding such controls, or at minimum evaluating against a pre-existing Trojan benchmark, is necessary before the claimed security-reliability result can be accepted.
minor comments (5)
  1. [Section III-A] The text "The original assertion from the NS31A(Definition6) RISC-V processor" refers to the wrong definition; NS31A is defined in Definition 5, while Definition 6 defines Ibex.
  2. [Table II] The row "11 CSR &" contains a stray ampersand in the Module Name column, which should be removed.
  3. [Abstract and Table I] The Abstract says "nearly 100% success" while Table I reports exactly 100% for all five modules; the paper should state explicitly whether any assertions were partially translated or dropped, or use precise numbers.
  4. [Eq. (1)] The definition of the triggering probability P for multi-bit signals could be clarified; the current example only shows the 1-bit case, leaving it unclear how the total number of combinations is counted when a Trojan condition involves specific bits of multi-bit signals.
  5. [Abstract] The phrase "rigorously tested against hardware Trojans" is misleading given the prompt design in Section III-B; a more accurate phrasing would be "tested against LLM-generated Trojans that were explicitly targeted at the translated assertions."

Circularity Check

2 steps flagged · score 8.0 of 10

Trojan validation is circular: ChatGPT is prompted to generate Trojans according to the translated assertions, so the reported 100% detection is a prompt-following check, not evidence of security.

  1. fitted input called prediction [Section III-B, Hardware Trojan development (Step 2)]
    "In the Task section, the prompt instructs ChatGPT to generate Trojans according to the translated assertions of the selected module under security verification, focusing on areas where these assertions are applied. In the Output Required section, it specifies the generation of two SystemVerilog files: one with the embedded Trojans in the RTL and another with test cases designed to activate the Trojans, which can later be verified through simulation."

    The validation population is generated from the very artifacts being validated. ChatGPT is given the module RTL together with the translated assertion RTL file, and the prompt directs it to produce Trojans 'according to the translated assertions' and to focus 'on areas where these assertions are applied,' while the test cases are 'designed to activate the Trojans.' Every generated Trojan is therefore, by construction, placed in the assertion-monitored signal space and accompanied by an activating stimulus. The TDER formula (Eq. 2) then counts how many of these self-targeted Trojans trip the assertions; 100% is the expected consequence of the prompt being followed, not an empirical property of the assertion set.

  2. self definitional [Section III-A, Assertion Translation (Step 1), Test Case generation step]
    "In the Test Case generation step, test cases are created based on the translated assertions, with further adjustments made to the security assertions as necessary."

    Translation success is self-validated: the test cases used to confirm a translated assertion are built from that same translated assertion, and the assertion can be revised until the test case passes. This verifies only internal consistency between the assertion and its self-generated testbench, not whether the translated assertion preserves an independently established security property. Thus the reported 100% translation rate for all modules is also a product of the evaluation procedure rather than an independent check against the original NS31A security properties or an external oracle.

full rationale

The paper's translation pipeline—signal identification, internal logic signal handling, multi-layer signal tracing, and dropping untranslatable signals—constitutes genuine engineering work and may be useful independent of the security claim. However, the central security-validation experiment in Step 2 is structurally circular. Section III-B states that the LLM is fed the translated assertion RTL file and is prompted to 'generate Trojans according to the translated assertions of the selected module under security verification, focusing on areas where these assertions are applied,' and to produce 'test cases designed to activate the Trojans.' Under this protocol, the Trojan set is defined by the assertions under test, and the accompanying test cases are designed to force those Trojans to fire. The TDER metric in Eq. (2) therefore measures whether ChatGPT followed the prompt, not whether the assertions detect realistic, independently specified hardware Trojans. The 100% detection rate in Table I is an artifact of this generation protocol; the Abstract and Section V claims of 'reliability in detecting security breaches' rest on that circular evidence. Section III-A similarly validates translations using test cases 'created based on the translated assertions' with assertions adjusted until they pass, which is a self-referential check. No self-citation chain is involved; the circularity is in the experiment design, where the validation set is generated from the objects being validated. Score 8 reflects that the headline security claim is forced by the construction of the Trojan generation task.

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

No numeric free parameters enter the TPI/TDER equations. The important uncontrolled choices are conceptual: the security semantics of signal mapping are assumed preserved, the LLM's prompt behavior is treated as a threat generator, and the module selection is inherited from prior work. These assumptions are load-bearing and untested.

assumptions (3)
  • domain assumption Signal mapping between NS31A and Ibex preserves the security semantics of an assertion.
    The translation methodology (Section III-A) replaces the original signals with mapped target signals and drops any signals not present, without proving that the mapped assertion expresses the same security property.
  • domain assumption ChatGPT-4-generated Trojans and test cases are representative of real hardware Trojan insertions.
    Section III-B uses LLM output as a proxy for real-world attacks; the paper calls these 'real-world scenarios' but provides no comparison to actual Trojan benchmarks.
  • domain assumption The five selected modules (PMP, CSR, DO, ETI, CF) are the security-critical modules.
    Heavily relies on prior work [23], [24] rather than a fresh threat analysis; the modules selection is taken as given.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Translating Common Security Assertions Across Processor Designs: A RISC-V Case Study." pith.science (2026). https://pith.science/paper/TDYHMU6C

@misc{pith2026250210194,
  author       = {Pith},
  title        = {Pith review of: Translating Common Security Assertions Across Processor Designs: A RISC-V Case Study},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/TDYHMU6C}},
  note         = {Machine review of arXiv:2502.10194}
}
read the original abstract

RISC-V is gaining popularity for its adaptability and cost-effectiveness in processor design. With the increasing adoption of RISC-V, the importance of implementing robust security verification has grown significantly. In the state of the art, various approaches have been developed to strengthen the security verification process. Among these methods, assertion-based security verification has proven to be a promising approach for ensuring that security features are effectively met. To this end, some approaches manually define security assertions for processor designs; however, these manual methods require significant time, cost, and human expertise. Consequently, recent approaches focus on translating pre-defined security assertions from one design to another. Nonetheless, these methods are not primarily centered on processor security, particularly RISC-V. Furthermore, many of these approaches have not been validated against real-world attacks, such as hardware Trojans. In this work, we introduce a methodology for translating security assertions across processors with different architectures, using RISC-V as a case study. Our approach reduces time and cost compared to developing security assertions manually from the outset. Our methodology was applied to five critical security modules with assertion translation achieving nearly 100% success across all modules. These results validate the efficacy of our approach and highlight its potential for enhancing security verification in modern processor designs. The effectiveness of the translated assertions was rigorously tested against hardware Trojans defined by large language models (LLMs), demonstrating their reliability in detecting security breaches.

Figures

Figures reproduced from arXiv: 2502.10194 by the authors.

Figure 1
Figure 1. Overview of the methodology for security assertion [PITH_FULL_IMAGE:figures/full_fig_p003_1.png] view at source ↗
Figure 2
Figure 2. Flowchart illustrating the process of assertion translation. [PITH_FULL_IMAGE:figures/full_fig_p003_2.png] view at source ↗
Figure 3
Figure 3. Example of translating an assertion for the Ibex [29] CSR [PITH_FULL_IMAGE:figures/full_fig_p004_3.png] view at source ↗
Figures from the paper (1 more)
Figure 4
Figure 4. Figure 4: Flowchart for hardware Trojan generation using [PITH_FULL_IMAGE:figures/full_fig_p004_4.png]

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

29 extracted references · 29 canonical work pages

  1. [1]

    The risc-v instruction set manual volume i: User-level isa document version 20191214-draft„

    RISC-V Foundation, “The risc-v instruction set manual volume i: User-level isa document version 20191214-draft„” Dec, 2019. [On- line]. Available: https://riscv.org/wp-content/uploads/2019/06/riscv- spec.pdf

    work page 2019

  2. [2]

    The risc-v instruction set manual volume ii: Privileged architecture document version 1.12-draft„

    RISC-V Foundation., “The risc-v instruction set manual volume ii: Privileged architecture document version 1.12-draft„” June,

    work page

  3. [3]

    [online] available: https://riscv.org/

    RISC-V , “[online] available: https://riscv.org/.” 2024

    work page 2024

  4. [4]

    Risc-v instruction set architecture extensions: A survey,

    E. Cui et al., “Risc-v instruction set architecture extensions: A survey,” IEEE Access , vol. 11, pp. 24 696–24 711, 2023

    work page 2023

  5. [5]

    Risc-v resource-constrained cores: A survey and energy comparison,

    I. Elsadek et al. , “Risc-v resource-constrained cores: A survey and energy comparison,” in 2021 19th IEEE International New Circuits and Systems Conference (NEWCAS) , 2021, pp. 1–5

    work page 2021

  6. [6]

    Towards automatic property generation for soc se- curity verification,

    X. Wang et al. , “Towards automatic property generation for soc se- curity verification,” in 2022 19th International SoC Design Conference (ISOCC), 2022, pp. 209–210

    work page 2022

  7. [7]

    Ieee standard for system, software, and hardware verification and validation - redline,

    “Ieee standard for system, software, and hardware verification and validation - redline,” IEEE Std 1012-2016 (Revision of IEEE Std 1012- 2012/ Incorporates IEEE Std 1012-2016/Cor1-2017) - Redline , pp. 1–465, 2017

    work page 2016

  8. [9]

    Accessible formal verification for safety-critical hard- ware design,

    J. Lach et al. , “ Accessible formal verification for safety-critical hard- ware design,” in RAMS ’06. Annual Reliability and Maintainability Symposium, 2006. , 2006, pp. 29–32

    work page 2006

Show all 29 references
  1. [10]

    Formal verification of hardware support for advanced encryption standard,

    A. Slobodova, “Formal verification of hardware support for advanced encryption standard,” in 2008 Formal Methods in Computer-Aided Design, 2008, pp. 1–4

    2008

  2. [11]

    A study on the assertion-based verification of digital ic,

    Y. Li et al., “ A study on the assertion-based verification of digital ic,” in 2009 Second International Conference on Information and Computing Science, vol. 2, 2009, pp. 25–28

    2009

  3. [12]

    Security and fault diagnosis-based assertion-based verification for fpga,

    S. Zhang et al. , “Security and fault diagnosis-based assertion-based verification for fpga,” in 2019 IEEE 19th International Conference on Software Quality, Reliability and Security Companion (QRS-C) , 2019, pp. 478–481

    2019

  4. [13]

    Systemverilog assertion based verification of amba- ahb,

    P . Gurha et al. , “Systemverilog assertion based verification of amba- ahb,” in 2016 International Conference on Micro-Electronics and Telecommunication Engineering (ICMETE) , 2016, pp. 641–645

    2016

  5. [14]

    Practical assertion-based formal verification for soc designs,

    P . Yeung et al. , “Practical assertion-based formal verification for soc designs,” in 2005 International Symposium on System-on-Chip , 2005, pp. 58–61

    2005

  6. [15]

    Property based formal security verification for hard- ware trojan detection,

    M. Qin et al. , “Property based formal security verification for hard- ware trojan detection,” in 2018 IEEE 3rd International Verification and Security Workshop (IVSW) , 2018, pp. 62–67

    2018

  7. [17]

    Fault attacks on access control in processors: Threat, formal analysis and microarchitectural mitigation,

    A. L. D. Antón et al. , “Fault attacks on access control in processors: Threat, formal analysis and microarchitectural mitigation,” IEEE Ac- cess, vol. 11, pp. 52 695–52 711, 2023

    2023

  8. [18]

    Invited: Formal verification of security critical hardware- firmware interactions in commercial socs,

    S. Ray et al., “Invited: Formal verification of security critical hardware- firmware interactions in commercial socs,” in 2019 56th ACM/IEEE Design Automation Conference (DAC) , 2019, pp. 1–4

    2019

  9. [19]

    Formal verification of security properties on risc- v processors,

    C. S. Chuah et al., “Formal verification of security properties on risc- v processors,” in 2023 21st ACM-IEEE International Symposium on Formal Methods and Models for System Design (MEMOCODE) , 2023, pp. 159–168

    2023

  10. [20]

    Security verification of risc-v system based on isa level information flow tracking,

    L. Wu et al. , “Security verification of risc-v system based on isa level information flow tracking,” in 2023 IEEE 32nd Asian Test Symposium (ATS), 2023, pp. 1–6

    2023

  11. [21]

    Formal verification of correctness and information flow security for an in-order pipelined processor,

    N. Dong et al. , “Formal verification of correctness and information flow security for an in-order pipelined processor,” in 2023 Formal Methods in Computer-Aided Design (FMCAD) , 2023, pp. 247–256

    2023

  12. [22]

    Transys: Leveraging common security properties across hardware designs,

    R. Zhang et al. , “Transys: Leveraging common security properties across hardware designs,” in 2020 IEEE Symposium on Security and Privacy (SP) , 2020, pp. 1713–1727

    2020

  13. [23]

    Hardware security in practice: Challenges and opportu- nities,

    N. Potlapally, “Hardware security in practice: Challenges and opportu- nities,” in 2011 IEEE International Symposium on Hardware-Oriented Security and Trust , 2011, pp. 93–98

    2011

  14. [24]

    Design of a generic security interface for risc-v processors and its applications,

    H. Oh et al. , “Design of a generic security interface for risc-v processors and its applications,” in 2018 International SoC Design Conference (ISOCC) , 2018, pp. 40–41

    2018

  15. [25]

    Reusing verification assertions as security checkers for hardware trojan detection,

    M. Eslami et al. , “Reusing verification assertions as security checkers for hardware trojan detection,” in 2022 23rd International Symposium on Quality Electronic Design (ISQED) , 2022, pp. 1–6

    2022

  16. [26]

    Sentaur: Security enhanced trojan assessment using llms against undesirable revisions,

    Jitendra Bhandari, Rajat Sadhukhan, Prashanth Krishnamurthy, Farshad Khorrami, Ramesh Karri , “Sentaur: Security enhanced trojan assessment using llms against undesirable revisions,” JuL,

  17. [27]

    Systemverilog assertions handbook,

    Ben Cohen, Srinivasan Venkataramanan, Ajeetha Kumari, and Lisa Piper , “Systemverilog assertions handbook,” 2016. [Online]. Available: https://systemverilog.us/sva4_preface.pdf

    2016

  18. [28]

    Ns31a : Risc-v 32bit cpu which supports iso26262 asil d,

    NSITEXE IP Solution , “Ns31a : Risc-v 32bit cpu which supports iso26262 asil d,” –. [Online]. Available: https://www.nsitexe.com/en/ip-solutions/ns-series/ns31a/

  19. [29]

    Ibex risc-v core,

    PULP platform , “Ibex risc-v core,” –. [Online]. Available: https://github.com/lowRISC/ibex

  20. [2019]

    Available: http://nic.vajn.icu/PDF/GigaDevice/RISCV- Privileged.pdf

    [Online]. Available: http://nic.vajn.icu/PDF/GigaDevice/RISCV- Privileged.pdf

  21. [2024]

    Available: https://arxiv.org/html/2407.12352v1

    [Online]. Available: https://arxiv.org/html/2407.12352v1

    arXiv

Pith tools

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