技術的概要：条件付き独立性を介したプロービングセキュリティの形式検証

問題定義

サイドチャネル攻撃は暗号方式のセキュリティに対して重大な脅威であり、これに対抗する対策としてマスキングの広範な採用を促している。マスキングは秘密値をシェアに分割し、中間値の任意の部分集合からの漏洩が根本的な秘密を明らかにしないことを保証する。しかし、特にISW プロービングモデル（敵対者が最大$t$個の中間値をプローブできるモデル）下において、マスキングされたアルゴリズムのセキュリティを証明することは、手作業で行う場合、極めて誤りやすいことで知られている。手作業によるセキュリティ証明にはいくつかの欠陥が特定されており、形式検証が必要とされている。

確率的分離論理は、ワンタイムパッドにおける入力独立性のような性質の検証には成功して適用されてきたが、マスキングされたアルゴリズムのプロービングセキュリティ（具体的には$t$-ノンインターフェアランス）の検証にはまだ利用されていない。既存の形式検証ツールは、しばしば置換ベースの方法や型推論に依存しており、マスキングに固有の複雑な条件付き独立性推論に必要なモジュール性や表現力が欠けている可能性がある。

手法

本研究は、シミュレータベースのセキュリティ定義と条件付き独立性の間に厳密な関連性を確立することにより、形式検証への新たなアプローチを提案する。この手法は、条件付き独立性について推論するために設計された確率的分離論理Lilacに依存している。

1. 理論的基盤：シミュレータと条件付き独立性

著者は、ノンインターフェアランスの標準的なシミュレータベースの定義を条件付き独立性の観点から言い換える。

• シミュレータベースの視点: マスキングされたアルゴリズムが安全であるとは、敵対者が観測する任意のプローブの集合$O$に対して、残りの秘密シェアにアクセスすることなく、入力シェアの部分集合$I$のみを用いて$O$の分布を生成できるシミュレータが存在する場合をいう。
• 条件付き独立性の視点: このセキュリティ要件は、観測値$O$が、公開入力シェア$I$が与えられたとき、秘密入力シェア（$\Delta \setminus I$）と条件付き独立であるという記述と等価である。形式的には、$O \perp (\Delta \setminus I) \mid I$と表される。

本論文は、この等価性が、確率空間の独立な組み合わせと分解（disintegration）による条件付けを用いて確率的独立性をモデル化する Lilac の意味論的枠組み内で成り立つことを示している。

2. Lilac の拡張

プロービングセキュリティに Lilac を適用するために、著者は元の Lilac 定式化には存在しなかった特定の証明規則を論理に追加する。

• 半グラフイド公理: 本論文は、条件付き独立性の半グラフイド公理（対称性、分解、弱結合、収縮）が Lilac の意味論内で成り立つことを証明する。これらの公理は、証明中に条件付き独立性の記述を操作するために不可欠である。
• 合成規則: 逐次合成と for ループに対して特に、ノンインターフェアランス性質の合成を処理するための新しい規則が導入される。これらの規則により、より小さなガジェットから構築された複雑なアルゴリズムのモジュール化された検証が可能となる。
• 所有と弱体化: 追加の規則は、確率変数の所有権に関する推論や、共有されていない入力や変数の部分集合を扱う際のノンインターフェアランス性質の弱体化を容易にする。

3. 検証フレームワーク

検証プロセスは以下の手順を含む。

1. 確率的プログラミング言語APPLで記述されたマスキングされたアルゴリズムを、Lilac 内のホア triples に翻訳する。
2. 確立された等価性（定理 V.1）を用いて、$(I, O)$-ノンインターフェアランスの検証を、特定の条件付き独立性ホア triple の証明に帰着させる。
   $$\{ \text{own } \Delta \} \ M \ \{ Y. \ C_{x \leftarrow I}(\text{own}(\Delta \setminus I) * \text{own } O) \}$$
3. 拡張された証明規則セット（新しい半グラフイド規則と合成規則を含む）を適用して、必要な帰結を導出する。

主要な貢献

1. 形式的な関連性: 本論文は、プロービングセキュリティのシミュレータベースの定義と、Lilac で表現可能な条件付き独立性性質との間の形式的な等価性を確立する。これにより、暗号学的セキュリティ概念と確率的分離論理の間のギャップが埋められた。
2. Lilac の拡張: 著者は、マスキングされたアルゴリズムの検証に必要な追加証明規則のスイートを提供する。これには、条件付き独立性の半グラフイド公理と、逐次合成およびループのための合成規則が含まれる。
3. ケーススタディ: このアプローチの有効性は、Lilac を用いて 3 つの重要なアルゴリズムのプロービングセキュリティを形式検証することによって実証された。
   • MINIADDREPNOISE: マスキングされた値に一様ノイズを追加するサブルーチン。
   • REFRESH: 漏洩の蓄積を防ぐためにシェアをリフレッシュする基本的なアルゴリズム。
   • SECMULT: 標準的なマスキング乗算アルゴリズム。
   • ADDREPNOISEER: Raccoon署名方式（NIST によるポスト量子暗号の標準化候補）で使用される変種。これが$t$-Strong Noninterference with Unshared Input（$t$-SNIU）性質を満たすことを証明する。

結果

本論文は、対象アルゴリズムのホア triple を成功裡に導出し、それらのノンインターフェアランス性質を確認した。

• MINIADDREPNOISEについては、観測された入力が与えられたとき、出力シェアが観測されていない入力シェアと条件付き独立であることを証明が示している。
• REFRESHについては、アルゴリズムが$t$-Strong Noninterference（$t$-SNI）を満たすことを証明が検証している。これは標準的なノンインターフェアランスよりも強い性質であり、高次マスキングにおける合成に不可欠である。
• SECMULTおよびADDREPNOISEERについては、証明は新しい合成規則を活用して、これらのアルゴリズムに固有のネストされたループと複雑なデータ依存関係を処理している。

ADDREPNOISEERの検証は特に重要である。これは、$t$-SNIU 性質に依存する Raccoon 署名方式のセキュリティ証明の主要なコンポーネントを検証するものである。

意義と主張

著者は、この研究が、マスキングされたアルゴリズムのプロービングセキュリティの形式検証に対する確率的分離論理（具体的には Lilac）の最初の適用であると主張している。セキュリティ証明を条件付き独立性推論に変換することにより、このアプローチは、既存の置換ベースまたは型推論ツールに対するモジュール化され、論理的に厳密な代替手段を提供する。

本論文は、シミュレータと条件付き独立性を結びつけるという根本的なアイデアは概念的に単純であるが、Lilac におけるその形式化は、標準的な積確率空間ではなく独立な組み合わせに依存する論理の性質上、技術的に容易ではないことを強調している。主要定理の成功裡な導出と、現実世界の暗号コンポーネント（Raccoon）への適用は、このフレームワークが複雑な高次マスキング方式の検証に viable であることを示している。

この研究は、その範囲に関して控えめであり、現在の結果はプロービングセキュリティの情報理論的設定に限定されていると述べている。著者は、このアプローチを計算論的設定に拡張することと、対話型定理証明器にこの手法を実装することを、将来の重要な研究課題として特定している。また、このフレームワークは、セキュアマルチパーティ計算に見られるような他のシミュレータベースのセキュリティ性質にも適用可能であると示唆している。