💻 computer science

Controller Datapath Aware Verification of Masked Hardware Generated via High Level Synthesis

この論文は、高水準合成（HLS）によって生成されたマスク済みハードウェアにおいて、リソース共有によるダミー信号が既存の検証ツールで誤検知（偽陽性）を引き起こす問題を解決し、コントローラ・データパスの構造を考慮した状態ごとの形式検証を行う新しい検証手法「MaskedHLSVerif」を提案するものである。

原著者： Nilotpola Sarma, Vaishali Ghanshyam Chaudhuri, Chandan Karfa

公開日 2026-03-20

📖 1 分で読めます☕ さくっと読める

CC BY 4.0

原著者： Nilotpola Sarma, Vaishali Ghanshyam Chaudhuri, Chandan Karfa

原論文は CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/) でライセンスされています。 ✨ これは以下の論文のAI生成解説です。著者が執筆または承認したものではありません。技術的な正確性については原論文を参照してください。免責事項の全文を読む

この論文は、**「暗号化されたハードウェアを、より安全に、かつ自動的に作るための新しい『検査方法』」**について書かれています。

専門用語を抜きにして、日常の例え話を使って解説しますね。

1. 背景：なぜ「マスク」が必要なのか？

まず、暗号化された装置（例えばスマートカードやスマホのチップ）は、**「電力消費の側面からの攻撃（PSCA）」**という危険にさらされています。
これは、装置が動いている時の「電気の使用量」を盗み見ることで、中に入っている秘密の鍵を推測しようとする攻撃です。

これを防ぐために、**「マスク（覆い）」**という技術が使われます。

イメージ： 秘密の数字を「3 つの破片」に分け、それぞれにランダムな「ごみ（ノイズ）」を混ぜて処理します。
効果： 攻撃者が電力消費を見ても、ごみだらけの破片しか見えないので、元の秘密がバレません。

2. 問題点：自動生成ツールの「盲点」

以前は、この「マスク付きハードウェア」を設計するのは、熟練した職人が手作業で一つ一つ作っていました。しかし、それは時間がかかり、ミスも起きやすかったため、最近では**「HLS（High-Level Synthesis：高級言語合成）」**という自動生成ツールを使うようになりました。

HLS の役割： 設計者が書いた「C プログラム」を、自動的に「ハードウェアの設計図（RTL）」に変換してくれる便利なロボットです。

しかし、ここに大きな落とし穴がありました。

HLS の性格： このロボットは「セキュリティ」を重視して作られていません。「いかに速く、安く（部品数を減らして）動くか」を最優先に考えます。
結果： 部品を共有するために、**「時間差で同じ部品を回す（マルチプレクサを使う）」**ような設計にしてしまいます。
既存の検査ツールの失敗： これまで使われていた「セキュリティ検査ツール（REBECCA など）」は、**「すべての部品が同時に動いている可能性」**を疑ってチェックしていました。
- 例え話： 自動車の工場検査で、「すべてのドアが同時に開いている状態」をチェックしようとしたら、実際には「運転席のドアが開いている時だけ助手席のドアは閉まっている」というルールがあるのに、検査ツールは「両方開いていたら危険だ！」と誤って警告を出してしまいました。
- 現象： 実際には安全なのに、**「誤検知（False Positive）」**を起こして、安全な設計を「危険だ」と誤って判定してしまっていたのです。

3. この論文の解決策：「状態ごとの検査」

著者たちは、この問題を解決するために**「MaskedHLSVerif（マスクド HLS 検証）」**という新しい検査方法を提案しました。

核心となるアイデア：
「機械が今、どの『状態（ステップ）』にいるか」を把握して、その瞬間に実際に動いている部品だけをチェックすればいいのではないか？

新しいアプローチのイメージ：
- 従来の方法： 工場の全工程を一度に全部見渡して、「あり得るすべての組み合わせ」をチェックする。（だから、あり得ない組み合わせまで疑って、誤検知が多かった）
- 新しい方法（MaskedHLSVerif）：
  1. 機械の動きを「状態 1」「状態 2」「状態 3」…と細かく区切る。
  2. 「状態 1」の時は、A という部品と B という部品しか動かないと分かっている。
  3. だから、「状態 1」の時は A と B だけをチェックし、他の部品は「今は動いていないから無視する」とする。
  4. これをすべての状態に対して行い、最後に「全部 OK なら、全体も OK」と判断する。

これにより、「実際にはあり得ない組み合わせ」まで疑う必要がなくなり、誤検知をゼロにしました。

4. 驚くべき発見：自動生成ツールの「裏技」

この新しい検査ツールを使って実験したところ、さらに面白いことが分かりました。

発見： HLS ツールは、設計を効率化するために「式を並べ替える（再結合）」という処理をすることがあります。
リスク： この「並べ替え」が、たまたま「マスク（覆い）のルール」を壊してしまい、**「一見安全そうだが、実は秘密が漏れている」**という欠陥を生んでしまうことがありました。
成果： 従来のツールはこの欠陥に気づけず、新しいツールだけが**「HLS が勝手にやってしまったミス」を正確に見つけ出し、警告することができました。**

まとめ

この論文は、以下のようなことを伝えています。

自動生成ツール（HLS）は便利だが、セキュリティ検査には「誤検知」を起こしやすい。
新しい検査方法（MaskedHLSVerif）を使えば、「機械が今何をしているか」を考慮して正確にチェックできる。
これにより、安全な設計を「危険」と誤って捨てるのを防ぎ、逆に、自動生成ツールが作り出した隠れた欠陥も発見できるようになった。

つまり、**「自動生成されたセキュリティ装置を、より賢く、正確に守るための新しい検査マニュアル」**が完成したという画期的な研究です。

論文「Controller–Datapath Aware Verification of Masked Hardware Generated via High-Level Synthesis」の技術的サマリー

この論文は、暗号アルゴリズムのハードウェア実装における**電力サイドチャネル攻撃（PSCA）**に対する対策として「マスキング」技術を採用する際、高レベル合成（HLS: High-Level Synthesis）ツールを用いて生成された回路のセキュリティ検証に関する課題と解決策を提案しています。

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

1. 背景と問題点 (Problem)

マスキングの重要性と課題:
電力サイドチャネル攻撃を防ぐためのマスキング（秘密情報をランダムなシェアに分割して処理する手法）は、ソフトウェアでは確立されていますが、ハードウェア実装では手動で行うと時間がかかり、エラーが発生しやすいです。そのため、検証済みのマスキングされたソフトウェアから HLS ツールを用いて自動的に RTL（レジスタ転送レベル）ハードウェアを生成するアプローチが注目されています。
HLS 最適化によるセキュリティリスク:
HLS ツールはセキュリティを考慮して設計されていないため、レイテンシや面積の最適化（式バランス、再結合、リソース共有など）を行う際、意図せずマスキングのセキュリティを破綻させる可能性があります。
既存検証ツールの限界（False Positives）:
既存のハードウェアマスキング検証ツール（例：REBECCA）は、主に固定されたデータパスを前提としています。しかし、HLS によって生成された回路は、リソース共有のために**有限状態機械（FSM）とマルチプレクサ（MUX）**を用いた時間分割多重データパスを持っています。
- 既存ツールは、FSM の制御により「実際には実行されない入力組み合わせ」もすべて検証対象として扱ってしまいます。
- その結果、実際には発生しない経路での漏洩を検出してしまう**偽陽性（False Positives）**が発生し、安全な設計でも「不安全」と誤判定されてしまいます。

2. 提案手法：MaskedHLSVerif (Methodology)

著者らは、HLS 生成回路の特性（FSM とデータパスの制御）を考慮した新しい検証フロー**「MaskedHLSVerif」を提案しました。この手法の核心は「状態ごとの検証（State-wise Verification）」**です。

状態ごとの設計分割:
元の HLS 生成 RTL 設計を、FSM の各状態（State）に対応する小さなサブ設計に分割します。
- 各状態 $S_x$ において、その状態で有効に動作するデータパスと、それ以前の状態で依存関係にある操作を含めて抽出します。
- これにより、その状態で実際に実行される入力組み合わせのみを考慮した設計が得られます。
有効な入力組み合わせの限定:
分割された各サブ設計に対して、REBECCA などの既存の形式検証ツールを適用します。
- 従来の手法では「構造的に可能なすべての入力」を検証していましたが、この手法では「その状態において FSM が実際に選択する入力のみ」を検証します。
- これにより、到達不可能な経路による偽陽性を排除し、正確なセキュリティ評価が可能になります。
再帰的なラベル付けと合成安全性:
各状態の設計に対して、元の設計の入力変数（シェア、マスク、公開値）に基づいてラベル付けを再帰的に適用します。これにより、各状態の検証結果が合成的に全体の設計の安全性を保証します。

3. 主要な貢献 (Key Contributions)

既存ツールの限界の特定:
HLS 生成回路におけるリソース共有データパスと FSM の存在が、既存の形式検証ツール（REBECCA など）に偽陽性を引き起こす根本的な原因であることを明らかにしました。
HLS 最適化の影響分析:
HLS の最適化（再結合、式バランスなど）がマスキングのセキュリティに与える具体的な影響を議論し、検証の必要性を説きました。
MaskedHLSVerif ツールフローの開発:
状態ごとのデータパスを抽出・抽象化し、既存の検証ツールを安全に適用できる新しい形式検証手法を開発しました。
実証実験:
6 つのベンチマーク（DOM, COMAR, HPC1, HPC2 によるカスケード乗算器、および PRESENT 暗号の S-Box）を用いた実験により、既存ツールが偽陽性を報告する設計を、提案手法が正しく「安全」と判定できることを示しました。また、HLS 最適化によって意図的に導入されたマスキング欠陥（再結合による漏洩）を検出できることも実証しました。

4. 実験結果 (Results)

ベンチマーク:
Vitis HLS (2022.2) を使用して生成された 6 つの暗号回路（DOM, COMAR, HPC1, HPC2 などのマスキング方式を用いた乗算器と PRESENT S-Box）を対象としました。
偽陽性の解消:
- 既存ツール（REBECCA）は、FSM を持つすべての HLS 生成設計において「不安全（False）」と誤判定しました。
- 提案手法（MaskedHLSVerif）は、これらすべての設計を正しく「安全（True）」と判定しました。
- TVLA（T-Test）による物理的な電力測定実験でも、これらの設計が実際には 1 次セキュリティを満たしていることが確認され、提案手法の判定が正確であることが裏付けられました。
HLS 最適化欠陥の検出:
意図的に HLS の「式バランス（Expression Balancing）」最適化を有効にし、マスキングの順序を壊すようにした設計に対して、提案手法は 2 番目の状態においてセキュリティ欠陥を正しく検出しました。これにより、HLS 最適化によるセキュリティ侵害を検知できる能力も実証されました。

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

HLS 生成ハードウェアの検証の自動化:
本論文は、HLS によって生成されたマスキングハードウェアのセキュリティを検証する初の体系的なアプローチを提供しています。
設計効率と安全性の両立:
手動でのマスキング設計の負担を HLS に委ねつつ、その安全性を形式的に保証する手段を提供することで、暗号ハードウェアの設計サイクルを短縮しつつ、サイドチャネル攻撃への耐性を確保する道を開きました。
将来展望:
HLS 最適化がセキュリティに与える影響は未解明な部分が多く、本手法を用いてさらに多くの最適化パターンとセキュリティの関係を調査することが今後の課題として挙げられています。

総括:
この研究は、HLS 技術の利点を活かしつつ、その副作用（セキュリティリスク）を克服するための重要な枠組みを提供しており、次世代の安全な暗号ハードウェア設計プロセスにおいて不可欠な要素となります。