論文「Assertain: Automated Security Assertion Generation Using Large Language Models」の技術的サマリー

本論文は、IEEE MDTS 2026 において発表される予定の、ハードウェアセキュリティ検証における新たな自動化フレームワーク「Assertain」に関するものです。大規模言語モデル（LLM）を活用し、RTL 設計と脅威モデルを統合的に分析することで、セキュリティ固有の SystemVerilog アサーション（SVA）を自動生成する手法を提案しています。

以下に、問題定義、手法、主要な貢献、結果、および意義について詳細をまとめます。

1. 背景と課題 (Problem)

現代のシステムオンチップ（SoC）設計の複雑化に伴い、ハードウェアレベルのセキュリティリスクが増大しています。

• 手作業のボトルネック: 従来の形式検証（Formal Property Verification, FPV）は、セキュリティ特性や SVA の手動記述に依存しており、設計規模の増大や脅威モデルの進化に対応しきれていません。
• 既存 LLM 手法の限界: 既存の LLM によるアサーション生成手法は、以下の課題を抱えています。
  • 明示的な脅威意識の欠如。
  • 設計動作と標準化された脆弱性クラス（CWE: Common Weakness Enumeration）の体系的なマッピング不足。
  • 存在しない信号を参照する「幻覚（Hallucination）」や、形式検証ツールで実行不可能な文法エラーの発生。
  • 機能検証中心であり、セキュリティ特化の検証が不十分。

2. 提案手法 (Methodology)

Assertain は、高レベルの脅威意図と低レベルの設計アーティファクトを、厳密な形式検証アーティファクトに変換する 3 段階のアーキテクチャを採用しています。

第 1 段階：知識マッピング (Knowledge Mapping)

生成プロセスを現実の設計と脅威に接地させるため、標準化されたオントロジーへの整合を行います。

• 構造的アライメント ($M_{rtl}$): LLM を用いて入力 RTL 設計をハードウェアカテゴリ（メモリ、通信インターフェース、プロセッササブシステム等）に分類し、静的知識ベースに基づいて関連する CWE ID をマッピングします。
• 脅威ベクトル統合 ($M_{threat}$): ユーザーが指定した脅威モデル（例：サイドチャネル攻撃、権限昇格）を正規化し、対応する CWE ID に変換します。
• コンテキスト交差: 構造的に推定される脆弱性と、脅威モデルから導かれる脆弱性の共通部分（$C_{target} = C_{struct} \cap C_{threat}$）を特定し、ノイズを排除したターゲット検索空間を定義します。

第 2 段階：コンテキスト認識生成 (Context-Aware Generation)

特定された脆弱性に対して、LLM を用いて文脈を考慮したアサーションを生成します。

• プロンプト設計: 以下の 3 つのコンテキストを含みます。
  1. 役割: ハードウェアセキュリティエンジニアとしての役割定義。
  2. 脆弱性: 対象 CWE の定義、結果、具体例。
  3. 設計: 完全な RTL ソースコード（モジュールヘッダ、信号宣言、ロジック含む）の注入。
• 反復生成と構造化出力: 各脆弱性に対して LLM を $N$ 回反復クエリし、セキュリティシナリオ、自然言語特性、候補 SVA を含む構造化された Markdown テーブルを出力させます。これにより、確率的な生成の限界を克服し、カバレッジを最大化します。
• ルールベースの制約: 生成される SVA に対して、文法規則（|-> や |=> の適切な使用）、タイミング制約（リセット処理、クロック同期）、信号整合性（存在しない信号の参照禁止）などの厳格なルールを適用します。

第 3 段階：自己反射リファインメント (Self-Reflection Refinement)

LLM の出力に含まれる幻覚や構文エラーを修正するフェーズです。

• 検証とフィルタリング: 生成されたアサーションと完全な RTL ソースを照合し、存在しない信号や未定義の識別子を参照するアサーションを除去します。
• 合成: 残った有効なアサーションを、コンパイル可能な .sva ファイルとして出力します。これにより、最終的な出力は構造的に堅牢で、実際の設計に基づいたものとなります。

3. 主要な貢献 (Key Contributions)

• 脅威意識型 CWE マッピング: 設計構造とユーザー指定の脅威モデルを統合し、関連する CWE に基づいてアサーションを生成するフレームワークの提案。
• 自己反射リファインメント機構: 生成されたアサーションの構文と意味的整合性を RTL ソースと照合して自動修正するメカニズムにより、実行可能な SVA の生成率を飛躍的に向上。
• 機能検証とセキュリティ検証の統合: 単なる機能検証だけでなく、セキュリティ原則（例：リプレイ攻撃防止、フェイルセーフ、役割分離）に基づいた「アーキテクチャ的ギャップ」を検出する能力。

4. 実験結果 (Results)

11 の代表的なハードウェア設計（Door_Lock, DMI_JTAG, AES, MIPS, UART など）を用いて、ベースラインとなる GPT-5 と比較評価を行いました。

• 性能向上:
  • 正しいアサーション生成数: ベースライン比 +61.22% 向上。
  • 一意な CWE カバレッジ: ベースライン比 +59.49% 向上。
  • アーキテクチャ的欠陥検出: ベースライン比 +67.92% 向上。
• 具体例:
  • Store_Unit や MMU などの設計では、正しいアサーション数がベースラインの 2 倍以上に増加しました。
  • MIPS 設計では、アーキテクチャ的欠陥の検出数が 8 から 15 に増加しました。
• ケーススタディ:
  • DMI_JTAG: エラー時のデータ漏洩防止やトランザクションの真正性検証など、セキュリティクリティカルな特性を自動生成。
  • UART: デバッグモード時の設定ビットの非公開化など、権限管理に関する特性を生成。
  • アーキテクチャ的ギャップ分析: 既存の RTL が「仕様通り」動作していても、セキュリティ原則（例：リプレイ攻撃防止のためのノンス生成、SEU 耐性、グッチ抵抗）に違反している場合、アサーションの失敗として検出し、設計の強化を促すことが示されました。

5. 意義と結論 (Significance & Conclusion)

Assertain は、ハードウェアセキュリティ検証の自動化において以下の点で画期的です。

• 手作業の削減と品質向上: 専門知識を必要とするセキュリティ特性の記述を自動化し、人的ミスを削減しながらカバレッジを拡大します。
• セキュリティアーキテクトとしての役割: 単に実装が仕様と合致するかを確認するだけでなく、「設計がセキュリティ原則を満たしているか」を評価し、潜在的な脆弱性やアーキテクチャ的欠陥を浮き彫りにします。
• 実用性: 生成されたアサーションは形式検証ツールで直接実行可能であり、実際の設計フローへの統合が容易です。

今後は、CWE 知識ベースの拡張や、リトリエール増強生成（RAG）を用いた仕様接地の強化、フル SoC プラットフォームでの評価が予定されています。この研究は、複雑化するハードウェア設計に対するセキュリティ保証の新たなパラダイムを提供するものです。