技術要約：ハードウェア設計における情報フローのための拡張シンボリック実行

問題提起

ハードウェア設計のセキュリティ検証には、ソース信号（入力）からシンク信号（出力）へどのように情報が流れるかを分析する必要があります。望まぬフローは、アクセス権限の違反、メモリリーク、または権限昇格を招く可能性があります。シンボリック実行（SE）は、インストルメンテーションなしでこれらのフローを追跡できる精密なツールですが、「パス爆発」問題、すなわち分岐点によって実行パスの数が指数関数的に増加する問題に直面します。さらに、ハードウェア設計はマルチクロックサイクルによる推論を通じて複雑さをもたらすため、入力から出力までの完全なフローを実現することが困難になります。既存のソリューションは、設計空間を制限したり、小さなクリティカルなコンポーネントのみを分析したりすることがよくあります。

対処すべき核心的な課題は、限定された時間枠内で、実現可能な情報フロー（データが実際に移動する真のパス）と、実現不可能なパス（実行時には起こり得ない静的解析のアーティファクト）をいかに効率的に区別し、これらのフローを駆動するための具体的な入力シーケンスを提供するかという点です。

手法：SEIF

著者らは、情報の流れを検証し、明示するために、シンボリック実行を静的解析で拡張した手法である SEIF（「セーフ」と発音）を提案しています。SEIFは、Verilog RTL設計における信号の接続性をオーバー近似する、静的に構築された情報フロー（IF）グラフ上で動作します。

この手法は、主に3つのフェーズで進行します。

1. グローバルに実現不可能なパスの削減

シンボリック実行を呼び出す前に、SEIFはIFグラフを分析して、論理的に不可能なパスを排除します。

• セグメンテーション: IFパスは、非ブロッキング代入に基づき、クロックサイクルの境界を示すセグメントに分割されます。
• 制約チェック: 各セグメントについて、フローが発生するために必要な条件が収集されます。SMTソルバは、**共充足可能性（co-satisfiability）**をチェックします。単一のクロックサイクルセグメント内の制約が互いに矛盾している場合（例：信号が同時にHighかつLowである必要がある場合）、そのパスはグローバルに実現不可能として破棄されます。

2. ガイド付きシンボリック実行

残りのパスに対して、SEIFはIFグラフによってガイドされたシンボリック実行を用い、設計の状態を通じた実現可能な実行パスを見つけ出します。

• ガイド付き探索: 実行エンジンは、現在のIFグラフセグメントを実現するために必要な特定のコード行を含む設計パスのみを辿るように制限されます。これにより、探索空間が大幅に縮小されます。
• クロックサイクル境界の削減: 各クロックサイクルにおいて、エンジンは現在のシンボリック状態が次のIFセグメントの条件を満たしているかを確認します。満たしていない場合、その分岐につながるパスは削減されます。
• ストール戦略: 重要な革新は、IFパスの進行を「ストール（一時停止）」させる能力です。現在の状態が次のセグメントの条件を満たせない場合、SEIFはIFパスのポインタを進めずに、マシンの状態を進めるために設計を1クロックサイクル分シンボリックに実行します。決定的なのは、ストール中に、SEIFが（以前のセグメントに蓄積された情報を上書きするような）パスを探索することを防ぐことです（例：レジスタがクリアされるのを防ぐ）。
• 探索ヒューリスティック: 本論文では4つの探索戦略を評価しています：
  1. Baseline 1: 継続またはストールのみ（組み合わせの網羅的探索）。
  2. Baseline 2: バックトラッキングのみ（ストールなし）。
  3. Stalling with Backtracking: ハイブリッドアプローチ。
  4. Stalling with UNSAT Core Heuristic: UNSATコアを用いて、制約の衝突を減らすストールパスを優先順位付けし、有効な次状態へと探索を効果的に導きます。

3. セマンティック分析と後処理

• 真のフローの検証: テキスト上のフローは存在するが実際の情報転送が行われないケース（例：y = x XOR x）を排除するために、SEIFはセマンティックチェックを実行します。
• リセット状態の検証: ツールは、見出された実行パスが設計のリセット状態から到達可能であるかどうかをチェックします。到達できない場合、そのパスは中間状態から始まっていると特定されます。

主な貢献

1. SEIFの定義: ハードウェアにおける情報フローを分析するために、静的解析（IFグラフ）とガイド付きシンボリック実行を組み合わせた新しい手法。
2. 実装: Z3ソルバを利用した、Sylviaシンボリック実行エンジンとHyperflowグラフツールチェーンの上に構築されたツール実装。
3. 探索ヒューリスティック: マルチクロックサイクルのパス探索の複雑さを管理するために、ストールをガイドするUNSATコアの使用を含む、特定の探索戦略の開発と評価。
4. 評価: 4つのオープンソース設計（OR1200、openMSP430、AKER Access Control、およびAESコア）を用いた包括的なテスト。

結果

評価は、12コアと62GBのRAMを備えたデュアルソケットサーバーで実施されました。

• パスの計上: SEIFは、静的に構築されたIFグラフのパスの**86〜90%**を、実現可能な設計パスを見つけるか、あるいはそのパスが実行不可能であることを証明することによって、正常に計上しました。
• 真のフロー: 計上されたパスのうち、**58〜77%**が真の情報フローとして特定されました。これは、静的IFグラフが強力な近似であることを示しています。
• パフォーマンス: SEIFは、平均4〜6秒で10〜12クロックサイクルの深さまでパスを網羅的に探索できます。
• 探索戦略の有効性: UNSAT Core Heuristicは他の戦略よりも優れており、ベースラインよりも26%多くの設計パスを見つけ出し、平均探索時間をパスあたり3〜6秒に短縮しました。また、非ヒューリスティックなアプローチと比較して、バックトラッキングの頻度を大幅に減少させました。
• スケーラビリティ: MSP430のプログラムカウンタに関するケーススタディにおいて、SEIFは16クロックサイクルの探索ホライゾン内で、19,060個のIFパスのうち**89.93%**の設計パスを見つけ出しました。

重要性と主張

本論文は、SEIFが、静的解析のアーティファクトと実際のセキュリティ違反を区別するプロセスを自動化することで、セキュリティ検証に新しい視点を提供すると主張しています。

• 精度: エンジニアが複雑なマルチサイクルフローを手動で追跡したり、入力シーケンスを推測したりする必要を排除します。
• 実行可能性: 違反が見つかった場合、SEIFは、リセットまたは中間状態のいずれかから設計を違反パスに沿って駆動するための、具体的な入力値のシーケンスを提供します。
• 効率性: 静的IFグラフを使用してシンボリック実行をガイドすることにより、SEIFは純粋なシンボリック実行に固有のパス爆発問題を回避し、純粋なSEよりも深いクロックサイクルや大きな設計の分析を可能にします。
• 限界: 著者らは、SEIFが仕様および設計における良性なヒューマンエラーに起因する欠陥を対象としていることを認めています。検証後に挿入される悪意のある合成ツール、製造、またはサプライチェーン攻撃（例：アナログトロイ）によって導入される欠陥を検出することはできません。また、再収束ファンアウト（reconvergent fan-out）のシナリオでは、すべての設計パスを網羅的に探索できない場合、誤った結果を報告する可能性があります。