ATLAS: AI-Assisted Threat-to-Assertion Learning for System-on-Chip Security Verification

• URL: http://arxiv.org/abs/2603.01170v1
• Date: Sun, 01 Mar 2026 16:20:47 GMT
• Title: ATLAS: AI-Assisted Threat-to-Assertion Learning for System-on-Chip Security Verification
• Abstract summary: ATLAS bridges standardized threat modeling and property-based formal verification for System-on-Chip (SoC) security.<n>By combining asset-centric analysis with threat model templates and multi-source context, ATLAS automates the transformation from vulnerability reasoning to formal proof.
• Score: 37.252166064253196
• License: http://creativecommons.org/licenses/by/4.0/
• 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.

Related papers

• Combating Knowledge Corruption in Agent Systems: A Byzantine-Tolerant Secure Collaborative RAG Framework [61.79960727298522]
  We propose SecureCollaRAG, a Byzantine-tolerant collaborative RAG framework.<n>Our approach enables agent system to securely verify document provenance through dynamic GNN-based credibility scoring.<n>Through extensive evaluations and formal analysis, we demonstrate that SecureCollaRAG maintains robustness against attackers under non-IID data distributions.
  arXiv  Detail & Related papers  (2026-08-05T02:13:37Z)
• Beyond Detection: Agentic Attack Synthesis and Simulation for Smart Contracts [9.850249387268157]
  KASS (Knowledge-Augmented Attack Synthesis and Simulation) is a multi-agent framework for executable smart contract exploit verification.<n>It decomposes automated exploit generation into planning, generation, and testing stages.<n>It produces structured attack plans that document exploitation flows, quantify potential asset losses, and serve as semantic false positive filters for static analysis tools.
  arXiv  Detail & Related papers  (2026-07-17T06:31:49Z)
• Large Language Models in Misinformation Ecosystems: Misuse, Defense, and Vulnerability [65.56750741053266]
  Large language models (LLMs) have transformed misinformation from a content-centric problem into a broader ecosystem-level security challenge.<n>In this paper, we introduce a role-layer framework to unify these risks and defenses.<n>The role characterizes LLMs as attackers, defenders, and vulnerable components of verification systems, while the layer dimension covers content, social contexts, evidence environments, and verification.
  arXiv  Detail & Related papers  (2026-07-11T17:04:17Z)
• Specification-Driven Development Benchmark: Security Knowledge Transition [0.0]
  This paper proposes a security knowledge operationalization approach for AI-assisted specification-driven development.<n>A Multilayer Specification Security Model represents security knowledge through traceable relations between system entities.<n>A Security Knowledge Transition Method transforms business and technical specifications into a validated security-enriched generation contract.
  arXiv  Detail & Related papers  (2026-05-29T12:36:48Z)
• Exploiting LLM Agent Supply Chains via Payload-less Skills [10.141577783380281]
  We introduce Semantic Compliance Hijacking (SCH), a payload-less supply chain attack targeting autonomous coding environments.<n>The SCH approach translates malicious goals into unstructured natural language instructions formatted as necessary compliance rules, leading the agent to generate and execute unauthorized code.<n>The findings demonstrate the pervasive nature of this threat, with SCH achieving peak success rates of up to 77.67% for confidentiality breaches.
  arXiv  Detail & Related papers  (2026-05-14T06:55:47Z)
• SecPI: Secure Code Generation with Reasoning Models via Security Reasoning Internalization [50.71047638695205]
  Reasoning language models (RLMs) are increasingly used in programming.<n>Yet, even state-of-the-art RLMs frequently introduce critical security vulnerabilities in generated code.<n>We present SecPI, a fine-tuning pipeline that teaches RLMs to internalize structured security reasoning.
  arXiv  Detail & Related papers  (2026-04-04T04:29:11Z)
• Assertain: Automated Security Assertion Generation Using Large Language Models [2.244201188680868]
  Assertain is an automated framework that integrates design analysis, Common Weaknession (CWE) mapping, and threat model intelligence to automatically generate security properties and executable SystemVerilog Assertions.<n>Assertain outperforms GPT-5 by 61.22%, 59.49%, and 67.92% in correct assertion generation, unique CWE coverage, and architectural flaw detection.
  arXiv  Detail & Related papers  (2026-04-02T03:51:35Z)
• ReasAlign: Reasoning Enhanced Safety Alignment against Prompt Injection Attack [52.17935054046577]
  We present ReasAlign, a model-level solution to improve safety alignment against indirect prompt injection attacks.<n>ReasAlign incorporates structured reasoning steps to analyze user queries, detect conflicting instructions, and preserve the continuity of the user's intended tasks.
  arXiv  Detail & Related papers  (2026-01-15T08:23:38Z)
• TeleAI-Safety: A comprehensive LLM jailbreaking benchmark towards attacks, defenses, and evaluations [46.98103424349245]
  Existing safety evaluation benchmarks and frameworks are often limited by an imbalanced integration of core components.<n>We present TeleAI-Safety, a modular and reproducible framework coupled with a systematic benchmark for rigorous safety evaluation.<n>With a curated attack corpus of 342 samples spanning 12 distinct risk categories, the TeleAI-Safety benchmark conducts extensive evaluations across 14 target models.
  arXiv  Detail & Related papers  (2025-12-05T07:23:30Z)
• The Trojan Knowledge: Bypassing Commercial LLM Guardrails via Harmless Prompt Weaving and Adaptive Tree Search [58.8834056209347]
  Large language models (LLMs) remain vulnerable to jailbreak attacks that bypass safety guardrails to elicit harmful outputs.<n>We introduce the Correlated Knowledge Attack Agent (CKA-Agent), a dynamic framework that reframes jailbreaking as an adaptive, tree-structured exploration of the target model's knowledge base.
  arXiv  Detail & Related papers  (2025-12-01T07:05:23Z)
• AI Bill of Materials and Beyond: Systematizing Security Assurance through the AI Risk Scanning (AIRS) Framework [31.261980405052938]
  Assurance for artificial intelligence (AI) systems remains fragmented across software supply-chain security, adversarial machine learning, and governance documentation.<n>This paper introduces the AI Risk Scanning (AIRS) Framework, a threat-model-based, evidence-generating framework designed to operationalize AI assurance.
  arXiv  Detail & Related papers  (2025-11-16T16:10:38Z)
• A.S.E: A Repository-Level Benchmark for Evaluating Security in AI-Generated Code [49.009041488527544]
  A.S.E is a repository-level evaluation benchmark for assessing the security of AI-generated code.<n>Current large language models (LLMs) still struggle with secure coding.<n>A larger reasoning budget does not necessarily lead to better code generation.
  arXiv  Detail & Related papers  (2025-08-25T15:11:11Z)
• LASA: Enhancing SoC Security Verification with LLM-Aided Property Generation [7.52190283487474]
  Formal property verification (FPV) provides the capability to model and validate design behaviors.<n>Current practices require significant manual efforts to create such properties, making them time-consuming, costly, and error-prone.<n>This paper presents LASA, a novel framework that leverages LLMs and retrieval-augmented generation (RAG) to produce non-vacuous security properties.
  arXiv  Detail & Related papers  (2025-06-22T01:21:03Z)
• A Systematic Classification of Vulnerabilities in MoveEVM Smart Contracts (MWC) [0.0]
  We introduce a dedicated vulnerability taxonomy for smart contracts built with Move.<n>Our taxonomy spans 37 categorized vulnerability types across six semantic frames.<n>MWC lays the foundation for more secure and verifiable contracts in next-generation blockchain systems.
  arXiv  Detail & Related papers  (2025-05-25T08:53:23Z)
• Towards Copyright Protection for Knowledge Bases of Retrieval-augmented Language Models via Reasoning [58.57194301645823]
  Large language models (LLMs) are increasingly integrated into real-world personalized applications.<n>The valuable and often proprietary nature of the knowledge bases used in RAG introduces the risk of unauthorized usage by adversaries.<n>Existing methods that can be generalized as watermarking techniques to protect these knowledge bases typically involve poisoning or backdoor attacks.<n>We propose name for harmless' copyright protection of knowledge bases.
  arXiv  Detail & Related papers  (2025-02-10T09:15:56Z)
• SeCodePLT: A Unified Platform for Evaluating the Security of Code GenAI [58.29510889419971]
  Existing benchmarks for evaluating the security risks and capabilities of code-generating large language models (LLMs) face several key limitations.<n>We introduce a general and scalable benchmark construction framework that begins with manually validated, high-quality seed examples and expands them via targeted mutations.<n>Applying this framework to Python, C/C++, and Java, we build SeCodePLT, a dataset of more than 5.9k samples spanning 44 CWE-based risk categories and three security capabilities.
  arXiv  Detail & Related papers  (2024-10-14T21:17:22Z)
• RESAA: A Removal and Structural Analysis Attack Against Compound Logic Locking [2.7309692684728617]
  This paper presents a novel framework, RESAA, designed to classify CLL-locked designs, identify critical gates, and execute various attacks to uncover secret keys. Results show that RESAA can achieve up to 92.6% accuracy on a relatively complex ITC'99 benchmark circuit.
  arXiv  Detail & Related papers  (2024-09-25T14:14:36Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.