ATLAS: システム・オン・チップのセキュリティ検証のための AI 支援威胁 - 断言学習

arXiv:2603.01170v2 Announce Type: replace-cross 要旨: この研究は、システム・オン・チップ（SoC）のセキュリティにおいて、標準化された威胁モデルとプロパティベースの形式検証を架け橋にする、LLM 駆動型枠組みである ATLAS を提案しています。脆弱性情報データベース（例：Common Weakness Enumeration (CWE)）から出発し、ATLAS は SoC 固有の資産を識別し、関連する弱点をマッピングし、検証用の断言ベースのセキュリティプロパティと JasperGold スクリプトを生成します。資産中心の分析、標準化された威胁モデルテンプレート、およびマルチソースの SoC コンテキストを組み合わせて、ATLAS は脆弱性情報からの推論から形式証明への変換を自動化します。3 つの HACK@DAC ベンチマークで評価された結果、ATLAS は 48 つの CWE のうち 39 つを検出し、それらのバグの 33 つに対して正しいプロパティを生成しました。これにより、自動化された知識駆動型の SoC セキュリティ検証は、設計時点で安全であるというパラダイムへと進展しています。

arXiv:2603.01170v2 Announce Type: replace-cross 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.