{"id":"d4cf7f70-1152-4d52-9964-1eab8f25e171","arxiv_id":"2502.10194","paper_version":1,"verdict":"REJECT","confidence":"HIGH","novelty_score":4.0,"correctness_risk":"high","formal_verification":"none","parameter_count":0,"one_line_summary":"A RISC-V assertion translation workflow is reported with 100% translation and Trojan detection, but the detection test is circular because the Trojans were invented from the assertions themselves.","lead":"The authors describe a method for reusing security-check assertions from one RISC-V processor in another, and they report 100% success translating 33 checks and catching 33 test Trojans. The catch: the Trojans were generated from the very assertions they are supposed to test, so the perfect detection rate is baked into the experiment.","discovery_kind":"new_application","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Validation of 100% Trojan detection is circular: ChatGPT is instructed to generate Trojans targeting the signals the translated assertions monitor, so the perfect detection rate is tautological, not evidence of security.","rationale":"I read the paper as claiming two things: a process for translating security assertions between RISC-V cores, and evidence that translated assertions reliably catch hardware Trojans. The translation workflow has plausible components (signal mapping, multi-layer handling), but the experimental validation is the load-bearing support for the reliability claim. Section III-B's prompt is decisive: it tells the LLM to build Trojans 'according to the translated assertions' and to focus on areas where assertions are applied. A Trojan generated to violate the exact antecedent/consequent structure of an assertion is, almost by definition, detectable by that assertion. The test cases are likewise generated by the same prompt to activate the Trojans. This setup makes the 100% detection rate a tautology rather than a security evaluation. The reader's weakest assumption identifies the same issue, and I agree with the REJECT verdict for the security-validation claim. To be concrete, the missing independent benchmark is the decisive gap; a single blind-Trojan experiment would settle whether the concern lands. No concerns about author conduct are raised; the issue is entirely with the experimental design as described in the manuscript.","tokens_in":8597,"tokens_out":2386,"duration_ms":41651,"concrete_test":"Run the same translated assertions against an independent set of Trojans created without knowledge of the assertions: for example, (a) Trojans from Trust-Hub or another public benchmark targeting PMP/CSR/DO/ETI/CF behavior, or (b) a fresh batch generated by ChatGPT with a prompt that forbids mentioning the assertion file and requires Trojan triggers to be drawn only from microarchitectural events not referenced in the assertions. Count detections under the same QuestaSim flow. If detection remains 100% on the blind set, the reliability claim is supported; if any Trojan escapes, the reported 100% is an artifact of prompt circularity and the security conclusion must be weakened.","verdict_should_be":"REJECT","load_bearing_attack":"The paper's central security claim, that translated assertions reliably detect security breaches, rests on the Step 2 procedure in Section III-B. The prompt explicitly instructs ChatGPT to 'generate Trojans according to the translated assertions of the selected module' and to focus 'on areas where these assertions are applied,' and to produce test cases designed to activate those Trojans. Under this construction, every generated Trojan is, by construction, aimed at exactly the behavior the assertions check; the subsequent 100% detection rate in Table I is then an artifact of the generation protocol, not an empirical property of the assertions. The paper presents no independent Trojan benchmark (e.g., Trust-Hub), no Trojans from a third party unaware of the assertions, and no negative-control prompt in which Trojan generation is forbidden from using assertion-relevant signals. Without such controls, the 'Detection %' column cannot distinguish a genuinely protective assertion set from assertions that merely encode the prompt's own targeting decisions. The claim in the Abstract and Section V, 'demonstrating their reliability in detecting security breaches,' is therefore unsupported by the reported experiment. The translation workflow itself may still be useful, but the security-validation evidence collapses because the experiment is a positive-control demonstration that the assertions can fire, not a test of whether they catch realistic hardware Trojans.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","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.","tokens_in":8916,"tokens_out":3701,"duration_ms":40270,"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":[{"comment":"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.\"","section":"Section III-B, Table I, Eq. (2)"},{"comment":"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.","section":"Section III-A, Step 5 (Test Case generation), Table I"},{"comment":"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.","section":"Section III-B and Table I"}],"minor_comments":[{"comment":"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.","section":"Section III-A"},{"comment":"The row \"11 CSR &\" contains a stray ampersand in the Module Name column, which should be removed.","section":"Table II"},{"comment":"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.","section":"Abstract and Table I"},{"comment":"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.","section":"Eq. (1)"},{"comment":"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.\"","section":"Abstract"}],"recommendation":"reject","confidential_remarks":"The paper's translation workflow may have practical value, but the central validation is circular and the security claim is unsupported. A revision that adds an independent Trojan benchmark, a negative control, and an independent oracle for translation correctness would constitute a substantially different experimental effort. As submitted, the main result—100% detection—is not informative. The paper also does not provide the exact ChatGPT prompts used, which would be needed for reproducibility."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Colleague,\n\nThe short version: the 100% Trojan detection result is an artifact of the experimental setup, but there is a real engineering artifact underneath—a manual workflow for translating 33 security assertions from the NS31A core to Ibex across five modules, with a worked example that is easy to follow. The translation itself seems plausible and the authors are transparent about their LLM prompt.\n\nWhat is genuinely new: the concrete NS31A-to-Ibex assertion translation, the signal-mapping procedure (direct, indirect, multi-layer, dropped signals), and the two metrics (TPI, TDER). None of these are deep, but the case study is documented in enough detail that a verification engineer could reproduce the translation steps.\n\nThe soft spot is load-bearing. In Step 2, the prompt explicitly instructs ChatGPT to generate Trojans 'according to the translated assertions' and to focus on assertion-applied areas, and the test cases are generated to activate those Trojans. So the assertions are guaranteed to fire by construction. The 100% detection rate in Table I is a positive control, not evidence of security effectiveness. There is no independent Trojan benchmark, no Trojans from an unaware third party, no negative-control prompt. This is not a minor caveat; it invalidates the paper's headline claim. The translation success is also self-assessed with hand-written test cases and no independent oracle, and the 'dropping untranslatable signals' step could silently weaken an assertion without any sensitivity analysis.\n\nI also note a small discrepancy: the abstract says 'nearly 100%' but the table reports exactly 100% everywhere; not a big deal, but the hedging in the abstract is inconsistent with the body.\n\nOn the citation pattern: prior work like Transys is acknowledged, and the novelty claim is appropriately modest about the method while overstating the validation. The paper does not cite any independent Trojan-detection benchmark or negative results, which is part of why the validation reads as circular.\n\nWho gets value from this? Verification engineers who want a starting point for manually mapping assertions between RISC-V cores. It could be useful as a technical report or an extended abstract with honest evaluation. As it stands, the central security conclusion should not be trusted, and a serious venue should require new experiments with independent Trojans before publication. For peer review, I would send it out with a clear request for major revision—the translation workflow deserves a look, but the validation needs to be rebuilt from the ground up.\n\nRegards,","headline":"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.","tokens_in":9340,"tokens_out":2666,"would_cite":false,"duration_ms":28148,"reading_group":"maybe","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":[],"pacs":[],"model":"deepseek-v4-flash","headline":"Translated security assertions catch all 33 LLM-made Trojans across RISC-V cores.","keywords":["security assertions","assertion translation","RISC-V","hardware Trojan detection","SystemVerilog assertions","processor security verification","LLM-generated Trojans","signal mapping"],"falsifier":"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.","tokens_in":8385,"feed_emoji":"🛡️","tokens_out":7513,"duration_ms":73327,"temperature":0.7,"pith_summary":"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.","feed_headline":"Translated security assertions catch all 33 LLM-made Trojans","feed_subtitle":"A RISC-V case study shows assertion reuse across processor designs detects every injected hardware Trojan in simulation.","key_machinery":"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.","core_discovery":"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.","pith_inferences":["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."],"forward_implications":["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."],"supporting_citations":[{"why":"Supplies the original security assertions on the NS31A core that the translation method starts from.","marker":"[19]"},{"why":"Provides the Ibex RISC-V core RTL, the target design whose signals receive the translated assertions.","marker":"[29]"},{"why":"Supplies the LLM-based method used to generate the hardware Trojans for validating the translated assertions.","marker":"[26]"},{"why":"Establishes the prior technique of reusing verification assertions as security checkers for hardware Trojan detection, which this work extends via translation.","marker":"[25]"},{"why":"Presents Transys, an earlier assertion-translation framework that lacks RISC-V-specific support and motivates the new methodology.","marker":"[22]"},{"why":"Defines the NS31A 32-bit RISC-V core, the source processor from which assertions and security properties are taken.","marker":"[28]"},{"why":"Documents the SystemVerilog assertion temporal constructs (##N, $past) that the translated assertions rely on.","marker":"[27]"},{"why":"Identifies the high-risk processor modules that justify the selection of PMP, CSR, DO, ETI, and CF for security verification.","marker":"[23]"}],"fun_headline_variants":["Assertion translation across RISC-V catches all 33 Trojans","100% assertion reuse success in RISC-V processor security","Ported assertions detect every LLM injection in RISC-V","Security assertions translate across processors, snag all Trojans","RISC-V assertion reuse: 100% translation, 100% Trojan detection"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"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.","fun_headline_variants_meta":{"raw":{"variants":["Assertion translation across RISC-V catches all 33 Trojans","100% assertion reuse success in RISC-V processor security","Ported assertions detect every LLM injection in RISC-V","Security assertions translate across processors, snag all Trojans","RISC-V assertion reuse: 100% translation, 100% Trojan detection"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000296,"raw_usage":{"total_tokens":1716,"prompt_tokens":938,"completion_tokens":778,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":554,"completion_tokens_details":{"reasoning_tokens":689}},"tokens_in":554,"tokens_out":778,"duration_ms":6319,"temperature":1.0,"reasoning_tokens":689,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-07T19:00:12.932327+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"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.","supporting_citations":[{"cited_title":"Systemverilog assertions handbook,","cited_arxiv_id":null,"evidence_quote":"Documents the SystemVerilog assertion temporal constructs (##N, $past) that the translated assertions rely on."},{"cited_title":"Formal verification of security properties on risc- v processors,","cited_arxiv_id":null,"evidence_quote":"Supplies the original security assertions on the NS31A core that the translation method starts from."},{"cited_title":"Ibex risc-v core,","cited_arxiv_id":null,"evidence_quote":"Provides the Ibex RISC-V core RTL, the target design whose signals receive the translated assertions."},{"cited_title":"Sentaur: Security enhanced trojan assessment using llms against undesirable revisions,","cited_arxiv_id":null,"evidence_quote":"Supplies the LLM-based method used to generate the hardware Trojans for validating the translated assertions."},{"cited_title":"Reusing verification assertions as security checkers for hardware trojan detection,","cited_arxiv_id":null,"evidence_quote":"Establishes the prior technique of reusing verification assertions as security checkers for hardware Trojan detection, which this work extends via translation."},{"cited_title":"Transys: Leveraging common security properties across hardware designs,","cited_arxiv_id":null,"evidence_quote":"Presents Transys, an earlier assertion-translation framework that lacks RISC-V-specific support and motivates the new methodology."},{"cited_title":"Ns31a : Risc-v 32bit cpu which supports iso26262 asil d,","cited_arxiv_id":null,"evidence_quote":"Defines the NS31A 32-bit RISC-V core, the source processor from which assertions and security properties are taken."},{"cited_title":"Hardware security in practice: Challenges and opportu- nities,","cited_arxiv_id":null,"evidence_quote":"Identifies the high-risk processor modules that justify the selection of PMP, CSR, DO, ETI, and CF for security verification."}],"review_version":1}