Paper deep dive
ATLAS: AI-Assisted Threat-to-Assertion Learning for System-on-Chip Security Verification
Ishraq Tashdid, Kimia Tasnia, Alexander Garcia, Jonathan Valamehr, Sazadur Rahman
Intelligence
Status: succeeded | Model: Gemma-4-26B-A4B | Prompt: intel-v1 | Confidence: 91%
Last extracted: 7/20/2026, 2:14:53 AM
Summary
The paper introduces ATLAS, an LLM-driven framework for System-on-Chip (SoC) security verification that automates the transformation from vulnerability knowledge (CWE/CVE/CAPEC) to formal assertion-based properties. ATLAS utilizes a standardized threat modeling template, a generated Threat Model Database (TMDB), and asset-centric analysis to identify SoC-specific assets, map relevant weaknesses, and generate JasperGold scripts. Evaluated on HACK@DAC benchmarks, it detected 39/48 CWEs and generated correct properties for 33 cases.
Entities (16)
Relation Signals (13)
ATLAS → targets → System-on-Chip
confidence 95% · System-on-Chip (SoC) security verification
ATLAS → uses → Large Language Model
confidence 95% · ATLAS, an LLM-driven framework
ATLAS → uses → LLM
confidence 95% · ATLAS is an LLM-driven framework
ATLAS → uses → Common Weakness Enumeration
confidence 95% · Starting from vulnerability knowledge bases such as Common Weakness Enumeration (CWE)
ATLAS → generates → Threat Model Database
confidence 92% · generate a threat model database of the common security weaknesses
ATLAS → analyzes → RTL
confidence 90% · analyzing generic asset definition, threat model database, and buggy SoC register transfer level (RTL) code
Threat Model Database → derivedfrom → Common Weakness Enumeration
confidence 90% · generate a threat model database of the common security weaknesses using standard template, LLM, and publicly available vulnerability repositories CWE
ATLAS → evaluatedon → HACK@DAC
confidence 90% · Evaluated on three HACK@DAC benchmarks
ATLAS → →
Cypher Suggestions (0)
No Cypher suggestions yet.
Abstract
Abstract:This work presents ATLAS, an LLM-driven framework that bridges standardized threat modeling and property-based formal verification for System-on-Chip (SoC) security. Starting from vulnerability knowledge bases such as Common Weakness Enumeration (CWE), ATLAS identifies SoC-specific assets, maps relevant weaknesses, and generates assertion-based security properties and JasperGold scripts for verification. By combining asset-centric analysis with standardized threat model templates and multi-source SoC context, ATLAS automates the transformation from vulnerability reasoning to formal proof. Evaluated on three HACK@DAC benchmarks, ATLAS detected 39/48 CWEs and generated correct properties for 33 of those bugs, advancing automated, knowledge-driven SoC security verification toward a secure-by-design paradigm.
Tags
Links
- Source: https://arxiv.org/abs/2603.01170v2
- Canonical: https://arxiv.org/abs/2603.01170v2
Trouble viewing inline? Open PDF directly →
Full Text
56,332 characters extracted from source content.
Expand or collapse full text
ATLAS: AI-Assisted Threat-to-Assertion Learning for System-on-Chip Security Verification Ishraq Tashdid 1∗ , Kimia Tasnia 1∗ , Alexander Garcia 1 , Jonathan Valamehr 2 , and Sazadur Rahman 1 1 Department of Electrical and Computer Engineering, University of Central Florida; 2 Intel Corporation 1 ishraq.tashdid, kimia.tasnia, alexander.garcia, mohammad.rahman@ucf.edu, 2 jonathan.k.valamehr@intel.com Abstract This work presents ATLAS, an LLM-driven framework that bridges standardized threat modeling and property-based formal verifi- cation for System-on-Chip (SoC) security. Starting from vulnera- bility knowledge bases such as Common Weakness Enumeration (CWE), the framework identifies SoC-specific assets, maps relevant weaknesses, and generates assertion-based security properties and JasperGold scripts for verification. By combining asset-centric anal- ysis with standardized threat model templates, it automates the transformation from vulnerability reasoning to formal proof. Eval- uated on three HACK@DAC benchmarks, ATLAS detected 39/48 CWEs and, out of that 39, ATLAS was able to generate correct prop- erties for 33 of the bugs, advancing automated, knowledge-driven SoC security verification toward a secure-by-design paradigm. Keywords Security verification, Threat Modeling, LLM for Security. 1 Introduction Integrated circuits (ICs) form the backbone of modern technolo- gies spanning artificial intelligence (AI), healthcare, autonomous systems, and defense, powering secure communication, precision- guided platforms, and advanced computing [20]. Modern ICs have evolved into highly integrated and interconnected Systems-on-Chip (SoCs) composed of diverse pre-designed intellectual property (IP) blocks. Due to the complexity, horizontally distributed business models involving untrusted supply chain entities, and the use of potentially malicious third-party IPs, every stage of SoC design can face a spectrum of security vulnerabilities [20]. Moreover, the semiconductor industry faces inherent risks from non-security- aware specifications, implementation flaws, and aggressive time- to-market demands [20]. As semiconductor systems underpin criti- cal infrastructure, ensuring their resilience demands a proactive, secure-by-design approach. With post-silicon vulnerability remedi- ation costs rising sharply [21], early identification of threats and integration of countermeasures are essential to protect national, system-level and organizational integrity. While functional verification relies on established behavioral rules from hardware descriptions, security verification remains chal- lenging because it lacks standardized security rules and policies. As a result, much of the process depends on threat modeling. However, conventional threat modeling approaches [14,36,40,49,50,53] are largely manual, error-prone, and unable to keep pace with grow- ing design complexity and evolving attack vectors. The National Vulnerability Database [55], including CWE [47], CVE [11], and ∗ Equal contribution. This work is licensed under a Creative Commons Attribution 4.0 International License. DAC ’26, Long Beach, CA, USA © 2026 Copyright held by the owner/author(s). ACM ISBN 979-8-4007-2254-7/2026/07 https://doi.org/10.1145/3770743.3804400 (a)(b) Figure 1: (a) Increasing hardware security vulnerabilities in RISC-V based SoCs. (b) Trend in CWE [47] and CVE [11] over the years. CAPEC [7], catalogs over 200,000 hardware and software flaws, yet current methods do not systematically use this knowledge for SoC security. Although recent efforts have leveraged these databases for threat modeling [15,45], they still lack the comprehensiveness required for SoC security verification. Likewise, existing security verification techniques, including formal verification [16,18,48], code analysis [2,31], hardware fuzzing [6,17,22,56], and penetra- tion testing [4,45,46], remain fragmented, manual, and hard to scale. In particular, they rely on handcrafted security constraints that are labor-intensive, error-prone, and require deep expertise [30]. Re- cent LLM-assisted property generation methods are also ad hoc, covering only a small subset of vulnerabilities and lacking gener- alization across the full CWE space [4,5,46,52]. With reported security issues increasing rapidly each year (Fig. 1), manual assess- ment is no longer feasible, making scalable and automated threat modeling and security verification essential. To address these limitations, we present ATLAS, a unified frame- work that transforms vulnerability knowledge into formal proof through contextual reasoning.First, ATLAS standardizes threat modeling using a comprehensive template that explicitly captures attack vectors ensuring consistency and completeness across de- signs.Second, we achieve scalability and adaptability by generating a threat model database of the common security weaknesses using standard template, LLM, and publicly available vulnerability repos- itories CWE [47], CVE [11], and CAPEC [10] as a continuously evolving knowledge base. We have made this database open source for helping research community.Third, ATLAS can automatically identify the SoC specifics assets and relevant threat models by ana- lyzing generic asset definition, threat model database, and buggy SoC register transfer level (RTL) code.Fourth, through contextual reasoning with abstract syntax tree (AST), RTL summary, and SoC specification document, ATLAS guides LLM in generating accu- rate, design-specific assertion-based security properties for formal verification. Evaluated on three HACK@DAC [23,25,26] bench- marks, ATLAS identified 39/48 relevant CWEs and produced correct properties for 33 of those cases (>82%), detecting violations and demonstrating vulnerability knowledge to formal proof. The rest of the paper is organized as follows - Sec. 2 discusses the publicly available vulnerability databases, related works in SoC security verification, and their limitations. Sec. 3 describes the asset arXiv:2603.01170v2 [cs.CR] 23 Apr 2026 DAC ’26, July 26–29, 2026, Long Beach, CA, USATashdid et al. centric threat modeling approach using standard template, adver- sary models, security knowledge base, and generic asset definition. Sec. 4 outlines assertion based security prorpty generation using SoC contexts and threat models from Sec. 3. Experimental results are presented in Sec. 5 before concluding the paper in Sec. 6. 2 Background In this section we provide a brief summary of the publicly known vulnerability databases that serves as the security knowledge for ATLAS, existing security verification methods, and their limitations. 2.1 Vulnerability Databases To ensure SoC security, one of the first thing required is finding a comprehensive repository of real-world vulnerability incidents. The vulnerability databases maintained by the MITRE Corporation, specifically, CWE [47] and CVE [11] represent the most comprehen- sive and reliable crowd-sourced repositories for security incidents across hardware and software domains. The CWE catalog defines and classifies abstract security weaknesses, such as improper privi- lege checks or insecure data paths, while CVEs document concrete instances of these weaknesses in specific products or platforms [37]. Fig. 1(b) shows that over the years, the number of identified CWEs and CVEs has grown significantly, reflecting both the increasing complexity of modern hardware systems and the expanding attack surface they present. For hardware security in particular, this rise underscores the urgent need for systematic, design-time mitiga- tion strategies. By standardizing and disseminating vulnerability knowledge, these databases form a foundational resource for future security-aware SoC development. 2.2 Related works and their limitations As stated previously, threat modeling is the foundation of secu- rity verification, providing a systematic way to identify and miti- gate vulnerabilities before they propagate to downstream design stages. Despite its importance, existing methodologies suffer from several limitations.1Manual approaches are becoming increas- ingly ineffective as design complexity and attack sophistication grow [27,32,39,42,54]. As attack methods evolve and the range of weaknesses expands, as shown in Fig. 1(a), these approaches fail to scale, limiting coverage and slowing response to new threats. 2The CWE and CVE databases discussed in Sec. 2.1 collectively contain over 200,000 hardware and software vulnerabilities, yet few techniques comprehensively leverage this knowledge to im- prove SoC security. 3 The lack of comprehensive threat modeling further reduces the effectiveness of security verification. Existing techniques can be broadly divided into static and dynamic methods. 4Static methods, including formal verification [16,18,48], con- colic testing [34,35], and code analysis [2,31], require engineers to translate high-level security requirements into formal assertions, creating substantial manual overhead and increasing susceptibility to human error.5Dynamic methods such as fuzzing [6,17,22,56] and penetration testing [3,51] improve runtime coverage but still depend on manually crafted feedback functions, limiting automa- tion. More importantly, current methods do not adapt well to an evolving threat landscape. Unlike area, power, and performance Table 1: Threat model template and example. TemplateCWE-1245 Threat Model AdversarySimple Hardware Adversary AssetsHardware State and Logic Integrity Attack surfaceHardware Interfaces and State Machine Logic VulnerabilitiesImproper or insecure FSM design ThreatsExploiting undefined or insecure FSM transitions Table 2: Adversary models in ATLAS with different capabilities. Adversary ModelCapabilities Unprivileged SoftwareLimited capability to run user-code System SoftwareAdmin/root access to system software Startup code/SMM 1 Can tamper the boot or SMM 1 code NetworkCan communicate with confidential services Software Side ChannelCan monitor/extract confidential metadata Simple HardwarePhysical access w/o expensive equipment/training Skilled HardwarePhysical access with skilled training and FA 2 tools Insider ThreatAnyone within the trusted supply chain 1 System management mode, 2 Failure analysis. flows, SoC security design lacks standardized constraints or rules to guide verification, which in turn limits emerging approaches such as fuzzing and formal verification [30]. Recent assertion-based and large language model (LLM)-generated property methods tar- get specific CWEs, but remain ad hoc, unscalable, and unable to generalize across the broader vulnerability space [4, 5, 45, 46, 52]. 3 Asset Centric Threat Modeling In this section we discuss how ATLAS performs asset centric threat modeling by defining a template and adversary models, leveraging vulnerability databases, and utilizing LLM to address the limitations of existing threat modeling methods highlighted in Sec. 2.2. 3.1 Threat Model Template The need for a universal standard is one of the most critical lim- itations of existing threat modeling methods.Therefore,ATLAS standardizesasetofelementsasatemplatethatmustbedefined forSoCthreatmodeling. Table. 1 shows the threat model template elements and an example for CWE-1245 [12]. The example threat model is kept concise for brevity. To the best of our knowledge, this is the first attempt to standardize threat modeling. •Adversaries: Different systems have a diverse threat landscape based on the entities involved in the design and development. Ad- versary models categorize different types of potential attackers by defining their scopes, capabilities, and access levels. The selected adversary model helps to decide whether a type of vulnerability can be exploited in a particular system. ATLAS utilizes the adver- sary models [41] summarized in Table 2 to provide a structured framework to identify attack scenarios and vulnerabilities. • Assets: It is the secret data, process, or element that must be protected. Any secondary asset utilized to protect a primary asset also worth to protect. Utilizing the asset definitions in Table 3, ATLAS performs an asset centric threat modeling in Sec. 3.5. •Attack Surfaces: The adversary is expected to utilize an inter- face to interact with or access an asset to exploit a vulnerability. It greatly depends on the type of the system, and adversary model. For instance, an unprivileged software adversary may leverage command prompt as an attack surface, wherever, debug interface could be more appealing for a simple hardware adversary. • Vulnerabilities: A vulnerability is a weakness or flaw in a sys- tem that can be exploited to compromise its security. For instance, a lack of bound checking (vulnerability) exploited by an adversary may result in a buffer overflow attack (threat). • Threats: When an adversary exploits a vulnerability it becomes a threat. For instance, in the previous example, buffer overflow attack is the threat in this scenario. Please note that many existing threat models confuse vulnerabilities with threats [28]. ATLAS recognizes them as distinct elements in the threat model. ATLAS: AI-Assisted Threat-to-Assertion Learning for System-on-Chip Security VerificationDAC ’26, July 26–29, 2026, Long Beach, CA, USA 3.2 Security Knowledge Source In ATLAS, we generate a threat model database (TMDB) that serves as the knowledge base for security verification in Sec. 4. Several factors motivate the need for such a database. 1 Functional verifi- cation has testbenches, coverage metrics, and well-defined correct- ness properties [20], whereas security verification lacks comparable structure. Designers must still manually infer which threats apply to an SoC, leading to the limitations discussed in Sec. 2.2.2The National Vulnerability Database [55] contains rich security knowl- edge, but it is too abstract, scattered, and unstructured for direct use in verification.3Human-driven threat modeling cannot keep pace with SoC complexity, diverse IP blocks, and the rapidly ex- panding hardware attack surface, which is why existing works cover only a limited subset of CWEs [16,45]. 4 Identifying as- sets in RTL is only part of the task; engineers must also determine which CWEs apply to each asset class.5Security verification [30] depends on accurate, repeatable mappings from weaknesses to assertion templates, making ad hoc generation error-prone and incomplete. A threat model database standardizes and organizes vulnerability knowledge into actionable, reusable vectors, enabling automated and consistent mapping of assets to relevant weaknesses and their corresponding property families. By providing repeatable security criteria and scalable coverage across designs and evolving threats, it becomes the foundation for automated, comprehensive SoC security verification. We have published this threat model database (https://github.com/KimiaTasnia/Threat-Model-Database- for-Hardware-Security) for security professionals and researchers. 3.3 Threat Model Database Generation Human Feedback Vulnerability Database Adversary Models Th reat Model Template Example Threat Model Th reat ModelsLLM Figure 2: LLM assisted threat model data- base generation in ATLAS. Several attack patterns (CAPEC) can exploit a product vulnerabil- ity (CVE) which suf- fers from a fundamen- tal weakness (CWE). For instance, both ‘CAPEC- 1: Accessing Functional- ity Not Properly Con- strained by ACLs’ and ‘CAPEC-180: Exploiting Incorrectly Configured Access Control Security Levels’ exploits the ‘CWE-1191: On-Chip Debug and Test Interface With Improper Access Control’ derived from CVE-2019-18827. Therefore, resistance to a specific attack pattern (e.g., CAPEC-1) does not necessarily make the developed hardware resilient against remaining attacks (e.g., CAPEC-180) exploiting the same weakness (CWE-1191). Hence, in ATLAS we develop individual threat model for each CWE [47] by following the template discussed in Sec. 3.1 to generate a threat model database (TMDB) of known security weaknesses. However, we include all the associated CVEs and CAPECs in prompts to cover known vulnerabilities connected to that CWE. Fig. 2 shows how we leverages GPT-5 to assist in threat model database generation using template (Sec. 3.1), security knowledge source (Sec. 3.2), example threat models, and human feedback. To construct the threat model database (TMDB), we began by man- ually creating a small set of high-quality example threat models using the standardized threat model template and adversary def- initions. These examples established the expected structure and depth of analysis. GPT-5 was then prompted with these examples along with CWE [47] and its associated CVE [11], and CAPEC [10] links to generate additional threat models for selected hardware CWEs, and each output was reviewed and refined through human feedback. The manually validated models were consolidated into a JSON-formatted dataset that included instructions, template fields, adversary descriptions, and exemplar input–output mappings. After providing GPT-5 with this context dataset, the model consistently produced complete and accurate threat models verified by human expert, enabling us to automatically generate the remaining Hard- ware Design CWEs and assemble a comprehensive TMDB covering all known hardware weaknesses [13]. We utilize this TMDB for SoC specific asset identification (Sec. 3.4) and threat modeling (Sec. 3.5). 3.4 SoC Specific Assets Detection ATLAS utilizes threat model database (TMDB) and a set of generic asset definition, to identify design assets and conduct an asset centric threat modeling. Fig. 3 shows the flow of detecting SoC assets and relevant threat models for security verification in Sec. 4. •In an SoC, assets refer to sensitive information and data that require protection from unauthorized access and safeguarding against various threats. ATLAS identifies these security critical assets in the RTL by providing GPT-5 a list of generic asset def- initions. We categorized 7 types of generic assets as shown in Table. 3 by analyzing the NVD [10,11,47] that exploits various types of assets in it’s database. And also the probable keywords connecting these assets in an SoC by conducting literature sur- vey [9, 44]. The Table. 3 is kept concise due to brevity. •With the help of TMDB and generic asset definition, LLM as- sisted in finding the potential security assets in the given buggy SoC RTL. Fig. 3(a) shows an example of “Runtime Integrity & State Resources” with its generic definition and LLM’s response to identify the associated assets in the OpenTitan Direct Mem- ory Access (DMA) module [33] utilized in several HACK@DAC competition [26]. Fig. 3(b) is the identified assets in the dma mod- ule which lists the assets type, specific signal names, role of the signals and reasoning behind it to be asset. 3.5 Threat Modeling with ATLAS Once ATLAS detects the SoC assets that designer must protect, it performs asset centric threat modeling at the RTL abstraction layer. First,we provide LLM both the SoC asset list from Sec. 3.4 and threat model database (TMDB) from Sec. 3.3 as shown in Fig. 4(a). The TMDB already has threat models for every hardware CWEs. This way ATLAS covers all known hardware security threats. Query1: You are a hardware security engineer expert in secrity analysis of the RTL designs. You are going to help in developing an asset centric threat modeling of an SoC. Provided: Threat Model Database * Ordering does not matter First you need to identify the assets from a buggy RTL code. Here is the generic asset definition you need to look for in this buggy RTL code- Generic Asset Definition- Runtime Integrity & State assets: 1. These assets relate to the ongoing, correct, and secure operation of the SoC after it has successfully booted. Their purpose is to maintain and prove the device’s trustworthiness during operation. 2. Device Integrity and Operation: The overall goal of ensuring the system runs as intended without crashing or being compromised. 3. Hardware State and Logic Integrity: The correctness of internal hardware components, like Finite State Machines, that control secure operations. 4. Keywords may include- "state_*", "defult_*", "measurement_*" // module dma ... endmodule A) DMA control / FSM (hardware state & logic integrity) 1) name: dma_ctrl_fsm signals: [dma_ctrl_reg, dma_ctrl_new, dma_ctrl_en] role: "Drives the whole DMA lifecycle" why_sensitive: "Corrupting/forcing state can skip PMP checks, double-execute, or stall system." 2) name: dma_phase_vector signals: [valid_reg, valid_new, valid_en, valid_o] role: "Runtime progress/attestation of what the DMA is doing right now." why_sensitive: "Downstream logic trusts it; spoofing can hide illegal transfers." # B) Security enforcement state (PMP gate for DMA) ................................................................................... # D) Handshake / abort control (system-wide operation integrity) ................................................................................... Query2: Now I will provide you a threat model database. This threat model database is generated from CWEs, where for each CWE there is a threat model. You need to find out the applicable CWEs from the threat model database which are pruned to affect these sensitive assets that you listed. Most applicable CWE threat models from your database- CWE-1257: Improper Access Control Applied to Mirrored or Aliased Memory Regions CWE-1245: Improper Finite State Machines (FSMs) in Hardware Logic CWE-1221: Incorrect Register Defaults or Module Parameters ......................................................................... LLM’s Response1 LLM’s Response2 Figure 3: Asset-centric threat modeling from generic asset defini- tions (Table 3) to SoC-specific asset detection, then CWE identifica- tion using the Threat Model Database (TMDB). DAC ’26, July 26–29, 2026, Long Beach, CA, USATashdid et al. Table 3: Generic assets definition for SoC specific assets detection. Asset TypeDefinitionKeywords Sensitive Data Confidential information. IP, firmware, or personal data. keys_*, pass_*, secret_* protected_*, user_* Boot Integrity Verifies and loads boot. Establishes hardware root of trust. boot_*, hash_*, rom_* otp_*, key_* Attestation Data & Measurement Reports Signed measurements of states. Stored in dedicated registers. pcr_*, measurement_* idev_* Parametric Data Device-specific non-volatile values. Used for identity and calibration. otp_*, trim_*, nvm_cfg_* uid_*, device_id_*, serial_* Privileged System Resources Privileged control registers. Accessible in trusted modes. debug_* , *_mode *_level Shared Resources Shared buses or memories. Arbitration to prevent leakage. ready_*, valid_*, dma_* req_*, grant_*, crossbar_* Runtime Integrity & State Resources Correctness of runtime states. FSM integrity and policy enforcement. state_*, default_* pcr_*, measurement_* Second,LLM runs a keyword mapping in the TMDB to match those assets in the database. For instance, for the DMA control/FSM assets in Fig. 3(b), ATLAS searched with the keywords (fsm, finite state machine, state, control flow, transition, deadlock) in the TMDB. It mapped these keywords in every CWE threat models and identified the most critical CWEs which are pruned to exploit those assets as shown in Fig. 3(d). The threat model database helped tremendously in this step since it has a detailed threat model with critical compo- nents like assets, threats, vulnerabilities explaining the scenarios for any potential weakness in a system. Finally,along with listing all the potential weaknesses, ATLAS identified the corresponding threat models for the detected CWEs present in the TMDB. In this way, ATLAS was able to generate threat models for all the possible hardware CWEs in an SoC. 4 Security Verification using Formal Proof With the CWE-based SoC threat models generated in Sec. 3, here we use formal proof to identify the vulnerabilities in a buggy SoC. 4.1 Rationale for Formal Verification Security bugs are often hidden or masked in rare input combina- tions, resets, or corner-cases. Constraint Random Verification (CRV) covers only a small subset of those cases, and when it triggers them, it takes long time to observe the impact. On the other hand, formal verification translates the design into a formal (logic-based) model and exhaustively checks whether it satisfies given properties. If a violating execution exists, the formal tool returns a minimal coun- terexample trace, otherwise, it produces a proof or correctness. This aligns with our security objective of turning each SoC threat model into a property that is either formally proven or demonstrated to be vulnerable through a concrete counterexample. Sec. 3 yields the SoC threat model with a set of relevant CWEs, however, not all are exploited in the RTL under review. To distin- guish actionable vulnerabilities from non-issues, ATLAS generates an assertion based security property for each relevant CWE, cap- turing its corresponding attack vectors in a form suitable for formal proof. A failing property indicates that the weakness represented by that CWE is concretely exploitable in the design, whereas a proven property suggests that the RTL upholds the corresponding security requirement under the stated assumptions. We therefore define three objectives for formal security verification.Obj1)Map each relevant CWE to one or more assertion property guided by the threat model (i.e., asset, attack surface).Obj2)Generate concrete SystemVerilog Assertions (SVA) and formal properties bound to real signals, modes, and resets.Obj3)Execute the properties in JasperGold, review proofs/counterexamples, and record outcomes. Buggy RTL SoC Threat Model (Relevant CWE) Generic Asset Definition SoC Assets Threat Model DB (All CWEs) LLM LLM (a) Section 3 Yosys/ PyVerilog Abstract Syntax Tree Design Document Security Property, Verification Script SoC RTL Summary Security Vulnerability (b) Section 4 SoC Context Figure 4: Overview of AI-assisted security verification flow by AT- LAS. (a) Asset-centric threat modeling, discussed in Sec. 3, using a generic asset definition, threat model database, and buggy SoC RTL code. The outcome of this step is SoC threat model of relevant CWEs. (b) Property-based security verification using SoC context (AST, RTL summary, and design document), threat model of the relevant CWEs. At the end of the section, we pair each objective (Obj) with a corresponding resolution (Res). 4.2 Why SoC Context Matters Formal proofs are only as strong as the properties they verify, and those properties must be grounded in the correct design context [30]. While ATLAS leverages LLMs to reduce human error, minimize reliance on domain-specific expertise, and improve scalability, an SoC RTL and threat model from Sec. 3 alone cannot provide the intent required to derive sound security constraints [19,43]. To produce meaningful assertions, the LLM must understand where an attacker interacts (attack surfaces), who controls inputs (ad- versary/controllability), what assets must be protected, and how the design behaves across modes, resets, and handshakes. Without these contexts, LLM-generated assertions risk being out-of-scoped, under-constrained, or misleading. Hence, to enhance the SoC design context, we combine three complementary sources.First, the design documentation of the SoC, which contains the specifications, interface specs, register maps, mode semantics, and trust boundaries.Second, the abstract syntax tree (AST) of the RTL that contains topological and struc- tural details of the hardware (e.g., inputs, outputs, wires, registers, parameters, states, clock/reset style). Andthird, a general summary of the SoC RTL, generated by LLM with security in mind. In the following subsections we discuss the role of each of the sources and perform an ablation study in Sec. 5 (Fig. 6). 4.2.1 Design Documents (D). Design documents are developed by architects, designers, and verification engineers and provide a rich view of intended behavior of the SoC that the base RTL cannot capture. They describe the human intended architecture, name the assets to be protected, and spell out privilege and lifecycle rules, interface semantics, and behavior [38]. For instance, as shown in Fig. 5, once we provide the OpenTitan Direct Memory Access (DMA) documentation [33] to LLM, it infers that the specification requires the DMA to enforce bounded memory ranges and Physical Memory Protection (PMP) checks and that the design must uphold a defined level of access control granularity. Additionally, this context lets us align the asset-centric CWE threat model from Sec. 3 with the design under review. One of the identified CWE in the DMA module is CWE-1190. Moreover, LLM can correlate that this is a potential violation since the module had no enable and it will trigger the start port whenever SoC is driven. Therefore, the documentation shows where the attack-surface lies for the RTL. 4.2.2 AST. As specified previously, ATLAS provides an AST of the SoC RTL code during assertion property generation by LLM. ATLAS: AI-Assisted Threat-to-Assertion Learning for System-on-Chip Security VerificationDAC ’26, July 26–29, 2026, Long Beach, CA, USA - Provided: AST 1. CWE-1245: Improper FSM.. 2. Accessing FSM States.. 3. dma_ctrl_reg states: IDLE, CHECK_LOAD, LOAD, CHECK_STORE, STORE, DONE, ABORT Query: Act like a formal verification engineer, and you are going to help generate security properties. Provided: Buggy RTL + Threat Model // module dma ... endmodule 1. Assessing RTL security features 2. CWE-1245: Improper FSM.. 3. I need to assess FSM states.. 4. If abort is issued when there is no active command running in dma, the dma gets stuck in a unknown state. LLM Formal Property Generation without Contextual Files property no_unreachable_states; @(posedge clk_i) disable iff (!rst_ni) (dma_ctrl_reg != CTRL_START_LOAD) && (dma_ctrl_reg != CTRL_START_STORE); endproperty - Provided: AST + D + RTL Summ 1. There is policy gating for LOAD/STORE; no debug waiver. 2. abort, done_i are possible security sensitive registers 3. I need to check if we use abort properly.. - Provided: AST + D 1. Reading Document.. LLM Formal Property Generation with Contextual Files * Does not understand the FSM states and security context behind the RTL. * Ordering does not matter Binds CWE-1245 to FSM control.Binds CWE-1245 to FSM control. Captures RTL FSM States.Captures RTL FSM States. Masters trust boundaries and privileges for DMA RTL. Masters trust boundaries and privileges for DMA RTL. Learns about designer intended FSM flow and escape behavior. Learns about designer intended FSM flow and escape behavior. Maps security sensitive registers.Maps security sensitive registers. Decisive cue on “what” to protect.Decisive cue on “what” to protect. Answers “who” drives the inputs.Answers “who” drives the inputs. Answers “where” is the attack- surface. Answers “where” is the attack- surface. property abort_escape; @(posedge clk_i) disable iff (!rst_ni) (dma_ctrl_reg == CTRL_ABORT && !done_i) |=> (dma_ctrl_reg != CTRL_ABORT); endproperty Rightfully captures that if we’re in CTRL_ABORT while done_i is 0, then we must not be in CTRL_ABORT (i.e., we must leave ABORT); matching with golden reference. Rightfully captures that if we’re in CTRL_ABORT while done_i is 0, then we must not be in CTRL_ABORT (i.e., we must leave ABORT); matching with golden reference. LLM ResponseLLM ResponseHuman QueryHuman Query (a) (b) (c) (d) (e) Figure 5: LLM–assisted security property generation. (a) The same prompt (buggy SoC RTL and Threat Model) is given to both methods. (b) Plain LLM: without context, LLM misreads the design intent and fails to derive the correct security property. (c) ATLAS: adding AST provides control and structural knowledge of the FSM behavior. (d) The design documents (D) then highlight the trust boundaries and attack-surface. (e) RTL summary exposes the sensitive registers. Taken together, ATLAS is able to generate the correct property. Treating this structure as a graph lets the LLM reason about control and data flow [29]. In practice, this guides LLM to verify who drives the signals in which conditions, trace fan-in/fan-out to policy gates, and enumerate legal state transitions before it ever writes an assertion. For example, with the DMA AST, the LLM matches CWE- 1245 from SoC threat model on improper finite state machines (FSM) usage with the abort signal (See Fig. 5.(b)). Hence, the AST guides LLM to flag that abort could persist or be X in paths that should be clean when done_i is low. This matches a known vulnerability that was actually exploited in the HACK@DAC 21 [25]. 4.2.3 RTL Summary. The RTL summary is a security-centric syn- opsis produced by the LLM directly from the source code. It gives LLM an objective perspective during property generation by high- lighting security critical assets, guardrails, rules and checks without relying on human hints. This reduces the bias, a concept similar to why we do CRV instead of directed verification. The summary also surfaces code-level nuances that are easy to miss in a non-security- centric design document. Revisiting the DMA example from Fig. 5, LLM is able to note what are the critical registers and assets that are vulnerable, (not explicitly stated in the design documentation). 4.3 CWE to Property Generation After obtaining the CWE-based SoC threat model from Sec. 3, we map it to assertion-based security properties using the contexts discussed in Sec. 4.2. Fig. 5 compares two pathways that start from the same prompt (Fig. 5(a)). In (b), the LLM uses only buggy SoC RTL and the TMDB and fails to generate the correct property. In contrast, under the ATLAS flow, when the same buggy SoC RTL and threat model from (a) are augmented with the additional contexts ((c) AST, (d) Design Documents, and (e) RTL summary), the LLM produces the correct security property in almost every case, and these map cleanly to formal proofs (Sec. 5.2.1).Res1) For CWE-1245 in Fig. 5, the LLM first reviews the general sys- tem behavior, register map, RTL scope, and I/O connectivity from the D. The AST then reveals where policy/privilege gating, re- set/initialization hygiene, FSM integrity, ordering, and control flow are implemented, including RTL details not explicit in the D. Next, a security-centric RTL summary helps bind assets, policies, and states, and provides the key cue to condition ATLAS on the adver- sary model. Using all three sources, the LLM performs an initial pruning asset(Summary)∩ attack-surface(D)∩ path(AST), or at minimum forms concrete hypotheses about how sensitive as- sets should behave in the RTL. Our experiments also showed that the ordering of these contexts has little to no effect.Res2)With the detailed signal names, state encodings, logical semantics, and interface rules, ATLAS then instantiates non-vacuity covers so an- tecedents are exercised, providing guideposts for SVA generation. Res3)Finally, the resulting properties act as design-rule checks for JasperGold [8]: the properties are emitted as assertion files together with a .tcl harness that compiles the DUT, applies constraints, and runs proofs. This yields the outcome targeted in Fig. 4. Inconclusive results can be refined by tightening or relaxing assumptions, adding clarification, and rerunning twice. Persistently inconclusive cases are flagged for manual review. 5 Results & Evaluation In this section, we evaluate ATLAS on three industry scale RISC- V based SoC designs. We report detection coverage, properties, and formal proof outcomes, compare against a manual proof base- line [43] as golden reference, and then ablate the three contexts. 5.1 Experimental Setting OpenTitan SoC [1] featured in the HACK@DAC benchmarks (’18, ’19, ’21) [23–25] offers a rich set of real-world security bugs, making it an ideal benchmark for assessing ATLAS. ATLAS is assisted by GPT-5 as the base LLM. Design documents for the buggy RTL are sourced from the OpenTitan documentation and repository [33]. ASTs are generated using Yosys [57] or PyVerilog with Slang for SystemVerilog support. RTL summary is generated by the LLM to minimize human bias. JasperGold is used for formal verification. 5.2 Evaluation 5.2.1 Benchmark Results. ATLAS runs automatically on each bench- mark in Table 4. To keep the process fast and predictable, we limit the search to at most three iterations per bug; unresolved cases are flagged for manual review. Most failures within this budget follow a common pattern: either the bug depends on subtle functional intent not stated in the public documentation, or the specification omits the exact corner case the property must capture. Across the three HACK@DAC [26] benchmarks, ATLAS shows strong performance. The Detected CWEs column in Table 4 lists the CWE-based SoC threat models generated by ATLAS as discussed in Sec. 3. For each bug, ATLAS often identifies multiple relevant CWEs. During secu- rity verification (Sec. 4), it then detects the correct exploited CWE (shown in bold in Table 4) by generating assertion-based security properties and checking them in JasperGold for formal proof. A checkmark (✓) in the property (Prop.) and formal verification (FV) columns of Table 4 indicates that ATLAS successfully generated (a) (b) Figure 6: TMDB ablation across HACK@DAC’18, ’19, and ’21. (a) Number of correct CWEs identified by an LLM without TMDB versus ATLAS with TMDB. (b) Context ablation on accurate properties. DAC ’26, July 26–29, 2026, Long Beach, CA, USATashdid et al. Table 4: Security verification by ATLAS across three HACK@DAC [26] benchmarks by detecting relevant CWE threat models, generating corresponding assertion based security properties, and performing verification by JasperGold. HACK@DAC18 [23]HACK@DAC19 [24]HACK@DAC21 [25] ModuleBugsDetected CWEs Prop. FVModuleBugsDetected CWEs Prop. FVModuleBugsDetected CWEs Prop. FV adbg_tapLogic bug Checks 31/32 bits Pwd not reset Reset broken 1221 , 1191, 1271 1298 , 1221, 1191 1329 , 1271, 276 1419, 1271, 1191 ✓ ✓ ✓ × ✓ ✓ ✓ × csr_regfileDebug exit issue Read/Write access Incorrect M-mode Incorrect update 1244 , 1191, 1243 1262 , 1220, 269 1262 , 1220, 269 1256 , 200, 203 × ✓ ✓ ✓ × ✓ ✓ ✓ dmi_jtagPass flag reset Write w/o pass Hardcoded key Unreachable state 1239, 1271, 1191 1245 , 1191, 1244 1329 , 321, 798 1245 , 1191, 1221 × ✓ ✓ ✓ × ✓ ✓ ✓ mux_funcWrong mux Out uncleared 1240 , 1245, 1221 325 , 226, 1271 ✓ ✓ ✓ ✓ commit_stage Interrupt ×2 Commit 1281 , 1262, 1220 1281 , 1241, 1271 × × × × csr_regfileDebug open Privilege leak 1220 , 1191, 1243 1262 , 1220, 269 ✓ ✓ ✓ ✓ riscv_cs_regWrong privilege1207 , 1262, 269✓axi_nodeImproper bypass1220 , 1191, 269 × ×aes_192Counter stuck1240 , 323, 330✓ apb_gpioLock writable Reset clears lock 1207 , 1220, 276 1206 , 276, 1271 × ✓ × ✓ arianeNo flush after atomic No flush after priv 1281 , 1206, 1271 1281 , 1191, 1241 ✓ ✓ ✓ ✓ reglk_wrapp.Locks disabled Locks dropped 1232, 1221, 276 1234, 1232, 1221 × × × × axi_address_dec. Errors ignored20, 703, 388 × ×controllerHalt w/o exception1207 , 1419, 1271✓ ×sha256_wrapp. Input uncleared1239, 226, 1271 × × periph_busDual overlap GPIO range alias Triple overlap 1260 , 1203, 1257 1257 , 1203, 1260 1260 , 1257, 1203 ✓ ✓ ✓ ✓ ✓ ✓ aes0_wrapp.Input uncleared Ungated debug Uncleared debug 226 , 1243, 1271 1243 , 1191, 1243 1258, 1243, 226 ✓ ✓ × ✓ ✓ × riscv_coreHalted access FSM hanged Incomplete case Insecure req 1298, 1191, 1262 1245 , 1241, 1271 1245 , 1241, 1271 1220 , 1262, 269 × ✓ ✓ ✓ × ✓ ✓ ✓ How to Read the Table CWE formatting: • Green = Correct; • Strikethrough = Undetected by ATLAS; • Blue Texts = Assumed correct (no baseline for 5 CWEs). • Unbolded CWEs = Relevant CWEs (Sec. 5.2.3) •✓/× Indicate pass/fail (Prop. and FV). acct_wrapp.Reset full access276 , 1221, 1220 × × rtc_clockRTC time bug1247 , 682, 1271✓dmaAbort sticky1245 , 1271, 1221✓ soc_intercon.Out-of-range1203 , 1260, 1257 × ×rsa_wrapp.Output uncleared226 , 1271, 1271✓ jtag_tap_topNo password1262 , 1191, 1220✓ ×riscv_periph.Hardcoded ROM1310, 1323, 1312 × × the assertion-based security property and detected the weakness in the given HACK@DAC [26] module. With our threat model database (TMDB), ATLAS detected 39/48 security weaknesses (CWEs) across the three HACK@DAC [26] benchmarks. More importantly, when the correct CWE was identified, ATLAS generated the correct property in more than 82% of the cases. When ATLAS does not detect the exact CWE, it still produces “rele- vant” CWEs from the SoC threat model in Sec. 3. Even when formal verification fails, the generated property is often still useful. Such failures often occur because the harness does not exercise the exact exploit path or because internal guards mask the issue under nomi- nal stimuli. In these cases, the property can still point to a real SoC weakness. For example, several control and privilege checks gener- ated by ATLAS were not proven in the given environment, yet they revealed missing controls or incomplete resets that require fixes, consistent with the golden reference [43]. We treat these cases as ac- tionable warnings rather than false alarms. When ATLAS succeeds, high-quality context greatly improves security verification: contexts with clear interface and state descriptions yield higher first-pass success rates. This is visible in Table 4, where ATLAS consistently detected the correct CWE and generated the appropriate prop- erty for well-documented blocks such as aes_192 and rsa_wrapper. By contrast, missed CWE detections usually correspond to under- specified designs. For example, in HACK@DAC’18 [23], the first adbg_tap bug is described only as a generic logic error, and the documentation does not specify the intended latch and mask be- havior. Similarly, in HACK@DAC’21 [25], the reset behavior of the dmi_jtag pass flag is not specified. In both cases, the lack of ex- plicit functional contracts makes automatic property construction difficult for ATLAS. To understand deeper into how contexts help, in the following subsection, we show how the TMDB and three SoC contexts remain essential to steer the LLM towards meaningful assertions. 5.2.2 Ablation Study. We quantify the effect of TMDB and each contexts (D, AST, RTL Summ) across HACK@DAC’18, ’19, and ’21. Looking at Fig. 6(a), removing TMDB completely collapses threat modeling and security verification. For CWE detection, an LLM-only baseline detects 6/20 on ’18, 3/11 on ’19, and 4/17 on ’21, which is less than 30% detection rate. In contrast, ATLAS identifies 17/20, 11/11, and 11/17, respectively, with the TMDB, highlighting how structured threat modeling can improve LLM performance. Moreover, what makes ATLAS capable lies in the three SoC con- texts. Ablation on Fig. 6(b) shows the same trend. When provided only one SoC context, formal verification detects≤5 accurate properties. ATLAS detects+10,+4, and+6 additional correct prop- erties in HACK@DAC18, 19, and 21 benchmarks corresponding to roughly 3×, 2.3×, and 2.5×improvement. It is appearant that, TMDB is the root of identifying the CWEs, which then, with the help of three SoC contexts, results to accurate property generation. 5.2.3 Relevant CWE and Property Generation. During CWE gener- ation from TMDB, ATLAS often lists more than one relevant CWE because the same asset can have multiple weaknesses. One may be truly exploited while a nearby rule on that asset still holds. In HACK@DAC’18 apb_gpio, a real weakness exists in the lock register where the key can be overwritten. ATLAS also proposed a related property for the same lock-register asset that checks whether the address decoding for the key is correct. Furthermore, our experi- ments showed strong correlation among CWEs. A single weakness can overlap with two CWEs that describe nearly the same rule using different terms. For instance, in csr_regfile from HACK@DAC’21, ATLAS detected CWE-1220 and CWE-1262 together for the same debug scenario. One emphasizes access control policy, while the other focuses on privilege enforcement. In practice, both capture the idea that entering debug must not weaken privilege. Hence, ATLAS reports both CWEs together. 6 Conclusion and Future Directions ATLAS bridges standardized threat modeling and property-based formal verification for SoC security. It builds a CWE-driven threat model database and combines design documents, AST, and RTL summaries to generate design-specific security assertions end-to- end, from asset identification to weakness mapping to formal proof. Across three HACK@DAC benchmark suites, ATLAS reliably iden- tifies vulnerabilities and produces correct formal properties with minimal human intervention, outperforming prior approaches and showing meaningful progress in SoC design and security verifica- tion. ATLAS: AI-Assisted Threat-to-Assertion Learning for System-on-Chip Security VerificationDAC ’26, July 26–29, 2026, Long Beach, CA, USA References [1]Joey Ah-kiow and Benjamin Tan. 2024. An Investigation of Hardware Security Bug Characteristics in Open-Source Projects. arXiv preprint arXiv:2402.00684 (2024). [2] Hasan Al Shaikh, Mohammad Bin Monjil, Kimia Zamiri Azar, Farimah Farahmandi, Mark Tehranipoor, and Fahim Rahman. 2023. Quardtropy: Detecting and quantifying unauthorized information leakage in hardware designs using g-entropy. In 2023 IEEE International Symposium on Defect and Fault Tolerance in VLSI and Nanotechnology Systems (DFT). IEEE, 1–6. [3]Hasan Al-Shaikh, Arash Vafaei, Mridha Md Mashahedur Rahman, Kimia Zamiri Azar, Fahim Rahman, Farimah Farahmandi, and Mark Tehranipoor. 2023. Sharpen: Soc security verification by hardware penetration test. In Proceedings of the 28th Asia and South Pacific Design Automation Conference. 579–584. [4]Avinash Ayalasomayajula, Rui Guo, Jingbo Zhou, Sujan Kumar Saha, and Farimah Farahmandi. 2024. Lasp: Llm assisted security property generation for soc verification. In Proceedings of the 2024 ACM/IEEE International Symposium on Machine Learning for CAD. 1–7. [5]Avinash Ayalasomayajula, Rui Guo, Jingbo Zhou, Sujan Kumar Saha, and Farimah Farahmandi. 2024. Lasp: Llm assisted security property generation for soc verification. In Proceedings of the 2024 ACM/IEEE International Symposium on Machine Learning for CAD. 1–7. [6]Kimia Zamiri Azar, Muhammad Monir Hossain, Arash Vafaei, Hasan Al Shaikh, Nu- run N Mondol, Fahim Rahman, Mark Tehranipoor, and Farimah Farahmandi. 2022. Fuzz, penetration, and ai testing for soc security verification: Challenges and solutions. Cryptology ePrint Archive (2022). [7]S Barnum. 2008. Common attack pattern enumeration and classification (CAPEC) schema. Department of Homeland Security (2008). [8]Cadence Design Systems, Inc. 2025. JasperGold Formal Verification Platform. Cadence Design Systems, San Jose, California, USA. Commercial formal verification tool suite for property checking, equivalence, and static verification. [9] Paul E. Calzada, Zahin Ibnat, Mark Tehranipoor, and Farimah Farahmandi. 2025. VerilogDB: The Largest, Highest-Quality Dataset with a Preprocessing Framework for LLM-based RTL Generation. https://arxiv.org/abs/2507.13369 [10]CommonAttackPatternEnumerationsandClassifications.[n. d.]. https://capec.mitre.org/. [11] Common Vulnerabilities and Exposures. [n. d.]. https://w.cve.org/. [12] CWE-1245: Improper Finite State Machines (FSMs) in Hardware Logic. [n. d.]. https://cwe.mitre.org/data/definitions/1245.html. [13]CWE VIEW: Hardware Design. [n. d.]. https://cwe.mitre.org/data/definitions/1194.html. [14]Fabio De Rosa, Nicolò Maunero, Paolo Prinetto, Federico Talentino, and Martina Trussoni. 2022. Threma: Ontology-based automated threat modeling for ict infrastruc- tures. IEEE Access 10 (2022), 116514–116526. [15]Isra Elsharef, Zhen Zeng, and Zhongshu Gu. 2024. Facilitating threat modeling by leveraging large language models. In Workshop on AI Systems with Confidential Computing. [16]Baleegh Ahmad et. al. 2022. Don’t cweat it: Toward cwe analysis techniques in early stages of hardware design. In Proceedings of the 41st IEEE/ACM International Conference on Computer-Aided Design. 1–9. [17]Muhammad Monir Hossain et. al. 2023. Socfuzzer: Soc vulnerability detection us- ing cost function enabled fuzz testing. In 2023 Design, Automation & Test in Europe Conference & Exhibition (DATE). IEEE, 1–6. [18]Jeyavijayan Rajendran et.al. 2016. Formal security verification of third party intellec- tual property cores for information leakage. In 2016 29th International conference on VLSI design and 2016 15th international conference on embedded systems (VLSID). IEEE, 547–552. [19]Kaiyan Chang et.al. 2024. Natural language is not enough: Benchmarking multi-modal generative AI for Verilog generation. In Proceedings of the 43rd IEEE/ACM International Conference on Computer-Aided Design. 1–9. [20]Farimah Farahmandi, M Sazadur Rahman, Sree Ranjani Rajendran, and Mark Tehra- nipoor. 2023. CAD for High-Level Synthesis. In CAD for Hardware Security. Springer International Publishing Cham. [21]Nusrat Farzana, Fahim Rahman, Mark Tehranipoor, and Farimah Farahmandi. 2019. Soc security verification using property checking. In 2019 IEEE International Test Conference (ITC). IEEE, 1–10. [22]Vasudev Gohil, Rahul Kande, Chen Chen, Ahmad-Reza Sadeghi, and Jeyavijayan Rajendran. 2024. MABFuzz: Multi-armed bandit algorithms for fuzzing processors. In 2024 Design, Automation & Test in Europe Conference & Exhibition (DATE). IEEE, 1–6. [23]HACK-EVENT. 2019. HACK@DAC 2018: SoC Security Benchmark. https://github. com/HACK- EVENT/hackatdac18 Accessed: 2025-11-14. [24] HACK-EVENT. 2019. HACK@DAC 2019: SoC Security Benchmark. https://github. com/HACK- EVENT/hackatdac19 Accessed: 2025-11-14. [25] HACK-EVENT. 2021. HACK@DAC 2021: OpenTitan SoC Benchmark. https://github. com/HACK- EVENT/hackatdac21 Accessed: 2025-11-14. [26]Hardware security challenge contest. [n. d.]. https://hackthesilicon.com/hackdac24/. [27]Intel’s stock drops 30% overnight - company sheds $39 billion in market cap. [n. d.]. https://w.tomshardware.com/pc-components/cpus/intels-stock-drops-30- overnight-company-sheds-dollar39-billion-in-market-cap. [28] Roger G Johnston. 2010. Being vulnerable to the threat of confusing threats with vulnerabilities. The Journal of Physical Security 4, 2 (2010), 30–34. [29] M Zafir Sadik Khan, Nowfel Mashnoor, Mohammad Akyash, Kimia Azar, and Hadi Kamali. 2025. SAGE-HLS: Syntax-Aware AST-Guided LLM for High-Level Synthesis Code Generation. arXiv:2508.03558 [cs.PL] https://arxiv.org/abs/2508.03558 [30]Rasheed Kibria, Farimah Farahmandi, and Mark Tehranipoor. 2024. A Survey on SoC Security Verification Methods at the Pre-silicon Stage. Cryptology ePrint Archive (2024). [31] Rasheed Kibria, M Sazadur Rahman, Farimah Farahmandi, and Mark Tehranipoor. 2022. Rtl-fsmx: Fast and accurate finite state machine extraction at the rtl for security applications. In 2022 IEEE International Test Conference (ITC). IEEE, 165–174. [32]Paul Kocher, Jann Horn, Anders Fogh, Daniel Genkin, Daniel Gruss, Werner Haas, Mike Hamburg, Moritz Lipp, Stefan Mangard, Thomas Prescher, et al.2020. Spectre attacks: Exploiting speculative execution. Commun. ACM 63, 7 (2020), 93–101. [33]lowRISC C.I.C. 2025. OpenTitan: Open source silicon root of trust (RoT) project. https://opentitan.org/. Accessed: 2025-11-12. [34]Yangdi Lyu, Alif Ahmed, and Prabhat Mishra. 2019. Automated activation of multiple targets in RTL models using concolic testing. In 2019 Design, Automation & Test in Europe Conference & Exhibition (DATE). IEEE, 354–359. [35]Yangdi Lyu and Prabhat Mishra. 2020. Scalable concolic testing of RTL models. IEEE Trans. Comput. 70, 7 (2020), 979–991. [36]Russ McRee. 2014. Microsoft threat modeling tool 2014: identify & mitigate. ISSA Journal 39 (2014), 42. [37]Peter Mell and Irena Bojanova. 2024. Hardware Security Failure Scenarios: Potential Weaknesses in Hardware Design. Technical Report. National Institute of Standards and Technology. [38]Xingyu Meng, Amisha Srivastava, Ayush Arunachalam, Avik Ray, Pedro Henrique Silva, Rafail Psiakis, Yiorgos Makris, and Kanad Basu. 2024. Nspg: Natural language processing-based security property generator for hardware security assurance. In Proceedings of the 61st ACM/IEEE Design Automation Conference. 1–6. [39]Microsoft Unveils Emergency Windows Update That Disables Intel’s Spectre Fix. [n. d.]. https://fortune.com/2018/01/29/microsoft-windows-intel-spectre-fix/. [40] The MITRE EMB3D Threat Model. 2024. https://emb3d.mitre.org/. [41]IntelSecureDevelopment:ThreatModeling.[n. d.]. https://w.intel.com/content/w/us/en/security/security-practices/secure- development-practices/threat-modeling.html. [42] Researchers Point to an AMD Backdoor—And Face Their Own Backlash. [n. d.]. https://w.wired.com/story/amd-backdoor-cts-labs-backlash/. [43]Jayden Rogers, Niyaz Shakeel, Divya Mankani, Samantha Espinosa, Cade Chabra, Kaki Ryan, and Cynthia Sturton. 2024. Security Properties for Open-Source Hardware Designs. arXiv:2412.08769 [cs.CR] https://arxiv.org/abs/2412.08769 [44] Dipayan Saha, Sujan Kumar Saha, Mark Tehranipoor, and Farimah Farahmandi. 2024. Empowering Hardware Security with LLM: The Development of a Vulnerable Hard- ware Database. [45] Dipayan Saha, Hasan Al Shaikh, Shams Tarek, and Farimah Farahmandi. 2025. ThreatLens: LLM-guided Threat Modeling and Test Plan Generation for Hardware Security Verification. arXiv preprint arXiv:2505.06821 (2025). [46]Dipayan Saha, Shams Tarek, Hasan Al Shaikh, Khan Thamid Hasan, Pavan Sai Nal- luri, Md Ajoad Hasan, Nashmin Alam, Jingbo Zhou, Sujan Kumar Saha, and Mark Tehranipoor. 2025. SV-LLM: An Agentic Approach for SoC Security Verification using Large Language Models. arXiv preprint arXiv:2506.20415 (2025). [47]MITRESoftwareandHardwareDesignCWEs.[n. d.]. https://cwe.mitre.org/index.html. [48]Pramod Subramanyan and Divya Arora. 2014. Formal verification of taint-propagation security properties in a commercial SoC design. In 2014 Design, Automation & Test in Europe Conference & Exhibition (DATE). IEEE, 1–2. [49]Ishraq Tashdid, Tasnuva Farheen, and Sazadur Rahman. 2025. SAFE-SiP: Secure Authentication Framework for System-in-Package Using Multi-party Computation. In Proceedings of the Great Lakes Symposium on VLSI 2025 (GLSVLSI ’25). Association for Computing Machinery, New York, NY, USA, 391–396. doi:10.1145/3716368.3735248 [50] Ishraq Tashdid, Tasnuva Farheen, and Sazadur Rahman. 2026. InterPUF: Distributed Authentication via Physically Unclonable Functions and Multi-party Computation for Reconfigurable Interposers. arXiv:2601.11368 [cs.CR] https://arxiv.org/abs/2601.11368 [51]Ishraq Tashdid, Valentina Terry, Jordan Merkel, Tasnuva Farheen, and Sazadur Rahman. 2025. BeyondPPA: Human-Inspired Reinforcement Learning for Post-Route Reliability- Aware Macro Placement. In 2025 ACM/IEEE 7th Symposium on Machine Learning for CAD (MLCAD). 1–12. doi:10.1109/MLCAD65511.2025.11189164 [52]Kimia Tasnia, Alexander Garcia, Tasnuva Farheen, and Sazadur Rahman. 2025. VeriOpt: PPA-Aware High-Quality Verilog Generation via Multi-Role LLMs. In 2025 IEEE/ACM International Conference on Computer Aided Design (ICCAD). IEEE. [53]Kimia Tasnia and Sazadur Rahman. 2025. OPL4GPT: An Application Space Exploration of Optimal Programming Language for Hardware Design by LLM. Association for Computing Machinery, New York, NY, USA, 981–987. https://doi.org/10.1145/3658617. 3697621 [54]This ’Demonically Clever’ Backdoor Hides In a Tiny Slice of a Computer Chip. [n. d.]. https://w.wired.com/2016/06/demonically-clever-backdoor-hides-inside- computer-chip/. [55]CVSSSeverityDistributionOverTime.[n. d.]. https://nvd.nist.gov/general/visualizations/vulnerability-visualizations/cvss- severity-distribution-over-time. [56] Timothy Trippel, Kang G Shin, Alex Chernyakhovsky, Garret Kelly, Dominic Rizzo, and Matthew Hicks. 2022. Fuzzing hardware like software. In 31st USENIX Security Symposium (USENIX Security 22). 3237–3254. [57]Clifford Wolf and Johann Glaser. 2013. Yosys – A Free Verilog Synthesis Suite. In Proceedings of the 21st Austrian Workshop on Microelectronics (Austrochip). Linz, Austria, 47–52.